Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
|- x e. _V |
2 |
|
vex |
|- y e. _V |
3 |
1 2
|
pm3.2i |
|- ( x e. _V /\ y e. _V ) |
4 |
3
|
a1i |
|- ( ph -> ( x e. _V /\ y e. _V ) ) |
5 |
4
|
ssopab2i |
|- { <. x , y >. | ph } C_ { <. x , y >. | ( x e. _V /\ y e. _V ) } |
6 |
3
|
biantru |
|- ( z = <. x , y >. <-> ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) ) |
7 |
6
|
exbii |
|- ( E. y z = <. x , y >. <-> E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) ) |
8 |
7
|
exbii |
|- ( E. x E. y z = <. x , y >. <-> E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) ) |
9 |
8
|
abbii |
|- { z | E. x E. y z = <. x , y >. } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) } |
10 |
|
ax6ev |
|- E. u u = x |
11 |
|
equcom |
|- ( u = x <-> x = u ) |
12 |
11
|
exbii |
|- ( E. u u = x <-> E. u x = u ) |
13 |
10 12
|
mpbi |
|- E. u x = u |
14 |
|
ax6ev |
|- E. v v = y |
15 |
|
equcom |
|- ( v = y <-> y = v ) |
16 |
15
|
exbii |
|- ( E. v v = y <-> E. v y = v ) |
17 |
14 16
|
mpbi |
|- E. v y = v |
18 |
|
idn1 |
|- (. y = v ->. y = v ). |
19 |
|
opeq2 |
|- ( y = v -> <. x , y >. = <. x , v >. ) |
20 |
18 19
|
e1a |
|- (. y = v ->. <. x , y >. = <. x , v >. ). |
21 |
|
idn2 |
|- (. y = v ,. x = u ->. x = u ). |
22 |
|
opeq1 |
|- ( x = u -> <. x , v >. = <. u , v >. ) |
23 |
21 22
|
e2 |
|- (. y = v ,. x = u ->. <. x , v >. = <. u , v >. ). |
24 |
|
eqeq1 |
|- ( <. x , y >. = <. x , v >. -> ( <. x , y >. = <. u , v >. <-> <. x , v >. = <. u , v >. ) ) |
25 |
24
|
biimprd |
|- ( <. x , y >. = <. x , v >. -> ( <. x , v >. = <. u , v >. -> <. x , y >. = <. u , v >. ) ) |
26 |
20 23 25
|
e12 |
|- (. y = v ,. x = u ->. <. x , y >. = <. u , v >. ). |
27 |
|
eqeq2 |
|- ( <. x , y >. = <. u , v >. -> ( z = <. x , y >. <-> z = <. u , v >. ) ) |
28 |
27
|
biimpd |
|- ( <. x , y >. = <. u , v >. -> ( z = <. x , y >. -> z = <. u , v >. ) ) |
29 |
26 28
|
e2 |
|- (. y = v ,. x = u ->. ( z = <. x , y >. -> z = <. u , v >. ) ). |
30 |
29
|
in2 |
|- (. y = v ->. ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) ) ). |
31 |
30
|
in1 |
|- ( y = v -> ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) ) ) |
32 |
31
|
eximi |
|- ( E. v y = v -> E. v ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) ) ) |
33 |
17 32
|
ax-mp |
|- E. v ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) ) |
34 |
33
|
19.37iv |
|- ( x = u -> E. v ( z = <. x , y >. -> z = <. u , v >. ) ) |
35 |
|
19.37v |
|- ( E. v ( z = <. x , y >. -> z = <. u , v >. ) <-> ( z = <. x , y >. -> E. v z = <. u , v >. ) ) |
36 |
35
|
biimpi |
|- ( E. v ( z = <. x , y >. -> z = <. u , v >. ) -> ( z = <. x , y >. -> E. v z = <. u , v >. ) ) |
37 |
34 36
|
syl |
|- ( x = u -> ( z = <. x , y >. -> E. v z = <. u , v >. ) ) |
38 |
37
|
eximi |
|- ( E. u x = u -> E. u ( z = <. x , y >. -> E. v z = <. u , v >. ) ) |
39 |
13 38
|
ax-mp |
|- E. u ( z = <. x , y >. -> E. v z = <. u , v >. ) |
40 |
39
|
19.37iv |
|- ( z = <. x , y >. -> E. u E. v z = <. u , v >. ) |
41 |
40
|
eximi |
|- ( E. y z = <. x , y >. -> E. y E. u E. v z = <. u , v >. ) |
42 |
|
19.9v |
|- ( E. y E. u E. v z = <. u , v >. <-> E. u E. v z = <. u , v >. ) |
43 |
42
|
biimpi |
|- ( E. y E. u E. v z = <. u , v >. -> E. u E. v z = <. u , v >. ) |
44 |
41 43
|
syl |
|- ( E. y z = <. x , y >. -> E. u E. v z = <. u , v >. ) |
45 |
44
|
eximi |
|- ( E. x E. y z = <. x , y >. -> E. x E. u E. v z = <. u , v >. ) |
46 |
|
19.9v |
|- ( E. x E. u E. v z = <. u , v >. <-> E. u E. v z = <. u , v >. ) |
47 |
46
|
biimpi |
|- ( E. x E. u E. v z = <. u , v >. -> E. u E. v z = <. u , v >. ) |
48 |
45 47
|
syl |
|- ( E. x E. y z = <. x , y >. -> E. u E. v z = <. u , v >. ) |
49 |
48
|
ss2abi |
|- { z | E. x E. y z = <. x , y >. } C_ { z | E. u E. v z = <. u , v >. } |
50 |
9 49
|
eqsstrri |
|- { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) } C_ { z | E. u E. v z = <. u , v >. } |
51 |
|
vex |
|- u e. _V |
52 |
|
vex |
|- v e. _V |
53 |
51 52
|
pm3.2i |
|- ( u e. _V /\ v e. _V ) |
54 |
53
|
biantru |
|- ( z = <. u , v >. <-> ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) ) |
55 |
54
|
exbii |
|- ( E. v z = <. u , v >. <-> E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) ) |
56 |
55
|
exbii |
|- ( E. u E. v z = <. u , v >. <-> E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) ) |
57 |
56
|
abbii |
|- { z | E. u E. v z = <. u , v >. } = { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) } |
58 |
50 57
|
sseqtri |
|- { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) } C_ { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) } |
59 |
|
df-opab |
|- { <. x , y >. | ( x e. _V /\ y e. _V ) } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) } |
60 |
|
df-opab |
|- { <. u , v >. | ( u e. _V /\ v e. _V ) } = { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) } |
61 |
58 59 60
|
3sstr4i |
|- { <. x , y >. | ( x e. _V /\ y e. _V ) } C_ { <. u , v >. | ( u e. _V /\ v e. _V ) } |
62 |
|
df-xp |
|- ( _V X. _V ) = { <. u , v >. | ( u e. _V /\ v e. _V ) } |
63 |
62
|
eqcomi |
|- { <. u , v >. | ( u e. _V /\ v e. _V ) } = ( _V X. _V ) |
64 |
61 63
|
sseqtri |
|- { <. x , y >. | ( x e. _V /\ y e. _V ) } C_ ( _V X. _V ) |
65 |
5 64
|
sstri |
|- { <. x , y >. | ph } C_ ( _V X. _V ) |
66 |
|
df-rel |
|- ( Rel { <. x , y >. | ph } <-> { <. x , y >. | ph } C_ ( _V X. _V ) ) |
67 |
66
|
biimpri |
|- ( { <. x , y >. | ph } C_ ( _V X. _V ) -> Rel { <. x , y >. | ph } ) |
68 |
65 67
|
e0a |
|- Rel { <. x , y >. | ph } |