Step |
Hyp |
Ref |
Expression |
1 |
|
elxp |
|- ( A e. ( ( _V X. _V ) X. _V ) <-> E. w E. z ( A = <. w , z >. /\ ( w e. ( _V X. _V ) /\ z e. _V ) ) ) |
2 |
|
ancom |
|- ( ( w = <. x , y >. /\ A = <. w , z >. ) <-> ( A = <. w , z >. /\ w = <. x , y >. ) ) |
3 |
2
|
2exbii |
|- ( E. x E. y ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. x E. y ( A = <. w , z >. /\ w = <. x , y >. ) ) |
4 |
|
19.42vv |
|- ( E. x E. y ( A = <. w , z >. /\ w = <. x , y >. ) <-> ( A = <. w , z >. /\ E. x E. y w = <. x , y >. ) ) |
5 |
|
elvv |
|- ( w e. ( _V X. _V ) <-> E. x E. y w = <. x , y >. ) |
6 |
5
|
anbi2i |
|- ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) <-> ( A = <. w , z >. /\ E. x E. y w = <. x , y >. ) ) |
7 |
|
vex |
|- z e. _V |
8 |
7
|
biantru |
|- ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) <-> ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) /\ z e. _V ) ) |
9 |
4 6 8
|
3bitr2i |
|- ( E. x E. y ( A = <. w , z >. /\ w = <. x , y >. ) <-> ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) /\ z e. _V ) ) |
10 |
|
anass |
|- ( ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) /\ z e. _V ) <-> ( A = <. w , z >. /\ ( w e. ( _V X. _V ) /\ z e. _V ) ) ) |
11 |
3 9 10
|
3bitrri |
|- ( ( A = <. w , z >. /\ ( w e. ( _V X. _V ) /\ z e. _V ) ) <-> E. x E. y ( w = <. x , y >. /\ A = <. w , z >. ) ) |
12 |
11
|
2exbii |
|- ( E. w E. z ( A = <. w , z >. /\ ( w e. ( _V X. _V ) /\ z e. _V ) ) <-> E. w E. z E. x E. y ( w = <. x , y >. /\ A = <. w , z >. ) ) |
13 |
|
exrot4 |
|- ( E. x E. y E. w E. z ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. w E. z E. x E. y ( w = <. x , y >. /\ A = <. w , z >. ) ) |
14 |
|
excom |
|- ( E. w E. z ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. z E. w ( w = <. x , y >. /\ A = <. w , z >. ) ) |
15 |
|
opex |
|- <. x , y >. e. _V |
16 |
|
opeq1 |
|- ( w = <. x , y >. -> <. w , z >. = <. <. x , y >. , z >. ) |
17 |
16
|
eqeq2d |
|- ( w = <. x , y >. -> ( A = <. w , z >. <-> A = <. <. x , y >. , z >. ) ) |
18 |
15 17
|
ceqsexv |
|- ( E. w ( w = <. x , y >. /\ A = <. w , z >. ) <-> A = <. <. x , y >. , z >. ) |
19 |
18
|
exbii |
|- ( E. z E. w ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. z A = <. <. x , y >. , z >. ) |
20 |
14 19
|
bitri |
|- ( E. w E. z ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. z A = <. <. x , y >. , z >. ) |
21 |
20
|
2exbii |
|- ( E. x E. y E. w E. z ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. x E. y E. z A = <. <. x , y >. , z >. ) |
22 |
12 13 21
|
3bitr2i |
|- ( E. w E. z ( A = <. w , z >. /\ ( w e. ( _V X. _V ) /\ z e. _V ) ) <-> E. x E. y E. z A = <. <. x , y >. , z >. ) |
23 |
1 22
|
bitri |
|- ( A e. ( ( _V X. _V ) X. _V ) <-> E. x E. y E. z A = <. <. x , y >. , z >. ) |