Metamath Proof Explorer

Theorem elvvv

Description: Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008)

Ref Expression
Assertion elvvv 
|- ( A e. ( ( _V X. _V ) X. _V ) <-> E. x E. y E. z A = <. <. x , y >. , z >. )

Proof

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 >. )