Theorem elvvv 4649

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

Assertion

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

Distinct variable group:   x, y, z, A

Proof of Theorem elvvv

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 4603	. 2 |- ( A e. ( ( _V X. _V ) X. _V ) <-> E. w E. z ( A = <. w , z >. /\ ( w e. ( _V X. _V ) /\ z e. _V ) ) )
2		anass 399	. . . . 5 |- ( ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) /\ z e. _V ) <-> ( A = <. w , z >. /\ ( w e. ( _V X. _V ) /\ z e. _V ) ) )
3		19.42vv 1891	. . . . . 6 |- ( E. x E. y ( A = <. w , z >. /\ w = <. x , y >. ) <-> ( A = <. w , z >. /\ E. x E. y w = <. x , y >. ) )
4		ancom 264	. . . . . . 7 |- ( ( w = <. x , y >. /\ A = <. w , z >. ) <-> ( A = <. w , z >. /\ w = <. x , y >. ) )
5	4	2exbii 1586	. . . . . 6 |- ( E. x E. y ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. x E. y ( A = <. w , z >. /\ w = <. x , y >. ) )
6		vex 2715	. . . . . . . 8 |- z e. _V
7	6	biantru 300	. . . . . . 7 |- ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) <-> ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) /\ z e. _V ) )
8		elvv 4648	. . . . . . . 8 |- ( w e. ( _V X. _V ) <-> E. x E. y w = <. x , y >. )
9	8	anbi2i 453	. . . . . . 7 |- ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) <-> ( A = <. w , z >. /\ E. x E. y w = <. x , y >. ) )
10	7, 9	bitr3i 185	. . . . . 6 |- ( ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) /\ z e. _V ) <-> ( A = <. w , z >. /\ E. x E. y w = <. x , y >. ) )
11	3, 5, 10	3bitr4ri 212	. . . . 5 |- ( ( ( A = <. w , z >. /\ w e. ( _V X. _V ) ) /\ z e. _V ) <-> E. x E. y ( w = <. x , y >. /\ A = <. w , z >. ) )
12	2, 11	bitr3i 185	. . . 4 |- ( ( A = <. w , z >. /\ ( w e. ( _V X. _V ) /\ z e. _V ) ) <-> E. x E. y ( w = <. x , y >. /\ A = <. w , z >. ) )
13	12	2exbii 1586	. . 3 |- ( 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 >. ) )
14		exrot4 1671	. . . 4 |- ( 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 >. ) )
15		excom 1644	. . . . . 6 |- ( E. w E. z ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. z E. w ( w = <. x , y >. /\ A = <. w , z >. ) )
16		vex 2715	. . . . . . . . 9 |- x e. _V
17		vex 2715	. . . . . . . . 9 |- y e. _V
18	16, 17	opex 4189	. . . . . . . 8 |- <. x , y >. e. _V
19		opeq1 3741	. . . . . . . . 9 |- ( w = <. x , y >. -> <. w , z >. = <. <. x , y >. , z >. )
20	19	eqeq2d 2169	. . . . . . . 8 |- ( w = <. x , y >. -> ( A = <. w , z >. <-> A = <. <. x , y >. , z >. ) )
21	18, 20	ceqsexv 2751	. . . . . . 7 |- ( E. w ( w = <. x , y >. /\ A = <. w , z >. ) <-> A = <. <. x , y >. , z >. )
22	21	exbii 1585	. . . . . 6 |- ( E. z E. w ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. z A = <. <. x , y >. , z >. )
23	15, 22	bitri 183	. . . . 5 |- ( E. w E. z ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. z A = <. <. x , y >. , z >. )
24	23	2exbii 1586	. . . 4 |- ( E. x E. y E. w E. z ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. x E. y E. z A = <. <. x , y >. , z >. )
25	14, 24	bitr3i 185	. . 3 |- ( E. w E. z E. x E. y ( w = <. x , y >. /\ A = <. w , z >. ) <-> E. x E. y E. z A = <. <. x , y >. , z >. )
26	13, 25	bitri 183	. 2 |- ( 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 >. )
27	1, 26	bitri 183	1 |- ( A e. ( ( _V X. _V ) X. _V ) <-> E. x E. y E. z A = <. <. x , y >. , z >. )

Syntax hints:   /\ wa 103   <-> wb 104   = wceq 1335   E.wex 1472   e. wcel 2128   _Vcvv 2712   <.cop 3563   X. cxp 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-opab 4026  df-xp 4592

This theorem is referenced by:  ssrelrel  4686  dftpos3  6209