Theorem elvv 4871

Description: Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.)

Assertion

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

Distinct variable group:   x, y, A

Proof of Theorem elvv

Step	Hyp	Ref	Expression
1		elxp 4829	. 2 |- ( A e. ( _V X. _V ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
2		vex 3016	. . . . 5 |- x e. _V
3		vex 3016	. . . . 5 |- y e. _V
4	2, 3	pm3.2i 461	. . . 4 |- ( x e. _V /\ y e. _V )
5	4	biantru 512	. . 3 |- ( A = <. x , y >. <-> ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
6	5	2exbii 1723	. 2 |- ( E. x E. y A = <. x , y >. <-> E. x E. y ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
7	1, 6	bitr4i 260	1 |- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )

Syntax hints:   <-> wb 189   /\ wa 375   = wceq 1448   E.wex 1667   e. wcel 1891   _Vcvv 3013   <.cop 3942   X. cxp 4810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pr 4612

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-opab 4434  df-xp 4818

This theorem is referenced by:  elvvv  4872  elvvuni  4873  elopaelxp  4885  ssrel  4901  elrel  4915  copsex2gb  4923  relop  4963  elreldm  5037  dmsnn0  5280  1stval2  6798  2ndval2  6799  1st2val  6807  2nd2val  6808  dfopab2  6835  dfoprab3s  6836  dftpos4  6979  tpostpos  6980  fundmen  7630  ssrelf  28230  dfdm5  30424  dfrn5  30425  brtxp2  30654  pprodss4v  30657  brpprod3a  30659  brimg  30710  funsndifnop  39116  fundmge2nop  39120  fun2dmnopgexmpl  39122