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