Theorem elvv 4998

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 4958	. 2 |- ( A e. ( _V X. _V ) <-> E. x E. y ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
2		vex 3074	. . . . 5 |- x e. _V
3		vex 3074	. . . . 5 |- y e. _V
4	2, 3	pm3.2i 455	. . . 4 |- ( x e. _V /\ y e. _V )
5	4	biantru 505	. . 3 |- ( A = <. x , y >. <-> ( A = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
6	5	2exbii 1636	. 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 369   = wceq 1370   E.wex 1587   e. wcel 1758   _Vcvv 3071   <.cop 3984   X. cxp 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-opab 4452  df-xp 4947

This theorem is referenced by:  elvvv  4999  elvvuni  5000  ssrel  5029  elrel  5043  copsex2gb  5051  relop  5091  elreldm  5165  dmsnn0  5405  1stval2  6697  2ndval2  6698  1st2val  6705  2nd2val  6706  dfopab2  6731  dfoprab3s  6732  dftpos4  6867  tpostpos  6868  fundmen  7486  ssrelf  26089  dfdm5  27724  dfrn5  27725  brtxp2  28049  pprodss4v  28052  brpprod3a  28054  brimg  28105  elopaelxp  30276