Theorem elopab 4708

Description: Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.)

Assertion

Ref	Expression
elopab	|- ( A e. { <. x , y >. | ph } <-> E. x E. y ( A = <. x , y >. /\ ph ) )

Distinct variable groups:   x, A   y, A

Allowed substitution hints:   ph( x, y)

Proof of Theorem elopab

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3087	. 2 |- ( A e. { <. x , y >. | ph } -> A e. _V )
2		opex 4667	. . . . 5 |- <. x , y >. e. _V
3		eleq1 2526	. . . . 5 |- ( A = <. x , y >. -> ( A e. _V <-> <. x , y >. e. _V ) )
4	2, 3	mpbiri 233	. . . 4 |- ( A = <. x , y >. -> A e. _V )
5	4	adantr 465	. . 3 |- ( ( A = <. x , y >. /\ ph ) -> A e. _V )
6	5	exlimivv 1690	. 2 |- ( E. x E. y ( A = <. x , y >. /\ ph ) -> A e. _V )
7		eqeq1 2458	. . . . 5 |- ( z = A -> ( z = <. x , y >. <-> A = <. x , y >. ) )
8	7	anbi1d 704	. . . 4 |- ( z = A -> ( ( z = <. x , y >. /\ ph ) <-> ( A = <. x , y >. /\ ph ) ) )
9	8	2exbidv 1683	. . 3 |- ( z = A -> ( E. x E. y ( z = <. x , y >. /\ ph ) <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )
10		df-opab 4462	. . 3 |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
11	9, 10	elab2g 3215	. 2 |- ( A e. _V -> ( A e. { <. x , y >. | ph } <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )
12	1, 6, 11	pm5.21nii 353	1 |- ( A e. { <. x , y >. | ph } <-> E. x E. y ( A = <. x , y >. /\ ph ) )

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1370   E.wex 1587   e. wcel 1758   _Vcvv 3078   <.cop 3994   {copab 4460

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 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642

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 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-opab 4462

This theorem is referenced by:  opelopabsbALT  4709  opelopabsb  4710  opelopabt  4712  opelopabga  4713  opabn0  4730  iunopab  4735  epelg  4744  elxp  4968  elopaba  5063  elcnv  5127  dfmpt3  5644  fmptsng  6012  0neqopab  6243  opabex3d  6668  opabex3  6669  fsplit  6790  isfunc  14897  qqhval2  26579  eulerpartlemgvv  26926  rtrclreclem.trans  27515  pellexlem5  29345  pellex  29347  elopaelxp  30306  clwlkswlks  30594  fmptsnd  30893  opelopab4  31615  dicelval3  35188