Theorem
-------
If s is a set then
ALL(a):[a e s <=> P(a)]
=> [ALL(a):[P(a) => Q(a)] <=> ALL(a):[a e s => Q(a)]]
Note: This proof was written with the aid of DC Proof 2.0. Download at http://www.dcproof.com
Notation
--------
& = AND-operator
=> = IMPLIES-operator
<=> = IF-AND-ONLY-IF-operator
ALL = Universal quantifier
Set = "Is a set" predicate
e = Set membership relation (epsilon)
User comments in blue font
Proof
-----
Let s be a set
1 Set(s)
Premise
Let s = {x : P(x)}
That is, suppose...
2 ALL(a):[a e s <=> P(a)]
Premise
'=>'
Prove: ALL(a):[P(a) => Q(a)] => ALL(a):[a e s => Q(a)]
Suppose...
3 ALL(a):[P(a) => Q(a)]
Premise
Prove: ALL(a):[a e s => Q(a)]
Suppose...
4 x e s
Premise
Apply definition of s
5 x e s <=> P(x)
U Spec, 2
6 [x e s => P(x)] & [P(x) => x e s]
Iff-And, 5
7 x e s => P(x)
Split, 6
8 P(x) => x e s
Split, 6
Apply Detachment Rule
9 P(x)
Detach, 7, 4
Apply premise
10 P(x) => Q(x)
U Spec, 3
11 Q(x)
Detach, 10, 9
Apply Conclusion Rule
As Required:
12 ALL(a):[a e s => Q(a)]
4 Conclusion, 4
'=>'
As Required:
13 ALL(a):[P(a) => Q(a)] => ALL(a):[a e s => Q(a)]
4 Conclusion, 3
'<='
Prove: ALL(a):[a e s => Q(a)] => ALL(a):[P(a) => Q(a)]
Suppose...
14 ALL(a):[a e s => Q(a)]
Premise
Prove: ALL(a):[P(a) => Q(a)]
Suppose...
15 P(x)
Premise
Apply definition of s
16 x e s <=> P(x)
U Spec, 2
17 [x e s => P(x)] & [P(x) => x e s]
Iff-And, 16
18 x e s => P(x)
Split, 17
19 P(x) => x e s
Split, 17
20 x e s
Detach, 19, 15
Apply premise
21 x e s => Q(x)
U Spec, 14
22 Q(x)
Detach, 21, 20
Apply Conclusion Rule
As Required:
23 ALL(a):[P(a) => Q(a)]
4 Conclusion, 15
'<='
As Required:
24 ALL(a):[a e s => Q(a)] => ALL(a):[P(a) => Q(a)]
4 Conclusion, 14
Join previous results
25 [ALL(a):[P(a) => Q(a)] => ALL(a):[a e s => Q(a)]]
& [ALL(a):[a e s => Q(a)] => ALL(a):[P(a) => Q(a)]]
Join, 13, 24
Apply Iff-And Rule
26 ALL(a):[P(a) => Q(a)] <=> ALL(a):[a e s => Q(a)]
Iff-And, 25
As Required:
27 ALL(a):[a e s <=> P(a)]
=> [ALL(a):[P(a) => Q(a)] <=> ALL(a):[a e s => Q(a)]]
4 Conclusion, 2