MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elopab Structured version   Unicode version

Theorem elopab 4697
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.
StepHypRef Expression
1 elex 3067 . 2  |-  ( A  e.  { <. x ,  y >.  |  ph }  ->  A  e.  _V )
2 opex 4654 . . . . 5  |-  <. x ,  y >.  e.  _V
3 eleq1 2474 . . . . 5  |-  ( A  =  <. x ,  y
>.  ->  ( A  e. 
_V 
<-> 
<. x ,  y >.  e.  _V ) )
42, 3mpbiri 233 . . . 4  |-  ( A  =  <. x ,  y
>.  ->  A  e.  _V )
54adantr 463 . . 3  |-  ( ( A  =  <. x ,  y >.  /\  ph )  ->  A  e.  _V )
65exlimivv 1744 . 2  |-  ( E. x E. y ( A  =  <. x ,  y >.  /\  ph )  ->  A  e.  _V )
7 eqeq1 2406 . . . . 5  |-  ( z  =  A  ->  (
z  =  <. x ,  y >.  <->  A  =  <. x ,  y >.
) )
87anbi1d 703 . . . 4  |-  ( z  =  A  ->  (
( z  =  <. x ,  y >.  /\  ph ) 
<->  ( A  =  <. x ,  y >.  /\  ph ) ) )
982exbidv 1737 . . 3  |-  ( z  =  A  ->  ( E. x E. y ( z  =  <. x ,  y >.  /\  ph ) 
<->  E. x E. y
( A  =  <. x ,  y >.  /\  ph ) ) )
10 df-opab 4453 . . 3  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
119, 10elab2g 3197 . 2  |-  ( A  e.  _V  ->  ( A  e.  { <. x ,  y >.  |  ph } 
<->  E. x E. y
( A  =  <. x ,  y >.  /\  ph ) ) )
121, 6, 11pm5.21nii 351 1  |-  ( A  e.  { <. x ,  y >.  |  ph } 
<->  E. x E. y
( A  =  <. x ,  y >.  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    = wceq 1405   E.wex 1633    e. wcel 1842   _Vcvv 3058   <.cop 3977   {copab 4451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-opab 4453
This theorem is referenced by:  opelopabsbALT  4698  opelopabsb  4699  opelopabt  4701  opelopabga  4702  opabn0  4720  iunopab  4725  epelg  4734  elxp  4959  elopaelxp  5015  elopaba  5057  elcnv  5121  dfmpt3  5640  fmptsng  6028  fmptsnd  6029  0neqopab  6278  opabex3d  6716  opabex3  6717  fsplit  6843  rtrclreclem3  12949  isfunc  15369  usgraop  24648  clwlkswlks  25056  brabgaf  27778  qqhval2  28295  eulerpartlemgvv  28701  dicelval3  34181  pellexlem5  35111  pellex  35113  opelopab4  36329
  Copyright terms: Public domain W3C validator