Theorem elvv 5047

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 5005	. 2 |- ( A e. ( _V X. _V ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
2		vex 3109	. . . . 5 |- x e. _V
3		vex 3109	. . . . 5 |- y e. _V
4	2, 3	pm3.2i 453	. . . 4 |- ( x e. _V /\ y e. _V )
5	4	biantru 503	. . 3 |- ( A = <. x , y >. <-> ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
6	5	2exbii 1673	. 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 252	1 |- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )

Syntax hints:   <-> wb 184   /\ wa 367   = wceq 1398   E.wex 1617   e. wcel 1823   _Vcvv 3106   <.cop 4022   X. cxp 4986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-opab 4498  df-xp 4994

This theorem is referenced by:  elvvv  5048  elvvuni  5049  elopaelxp  5061  ssrel  5079  elrel  5093  copsex2gb  5101  relop  5142  elreldm  5216  dmsnn0  5456  1stval2  6790  2ndval2  6791  1st2val  6799  2nd2val  6800  dfopab2  6827  dfoprab3s  6828  dftpos4  6966  tpostpos  6967  fundmen  7582  ssrelf  27681  dfdm5  29446  dfrn5  29447  brtxp2  29759  pprodss4v  29762  brpprod3a  29764  brimg  29815