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

Theorem elopab 4404
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 2908 . 2  |-  ( A  e.  { <. x ,  y >.  |  ph }  ->  A  e.  _V )
2 opex 4369 . . . . 5  |-  <. x ,  y >.  e.  _V
3 eleq1 2448 . . . . 5  |-  ( A  =  <. x ,  y
>.  ->  ( A  e. 
_V 
<-> 
<. x ,  y >.  e.  _V ) )
42, 3mpbiri 225 . . . 4  |-  ( A  =  <. x ,  y
>.  ->  A  e.  _V )
54adantr 452 . . 3  |-  ( ( A  =  <. x ,  y >.  /\  ph )  ->  A  e.  _V )
65exlimivv 1642 . 2  |-  ( E. x E. y ( A  =  <. x ,  y >.  /\  ph )  ->  A  e.  _V )
7 eqeq1 2394 . . . . 5  |-  ( z  =  A  ->  (
z  =  <. x ,  y >.  <->  A  =  <. x ,  y >.
) )
87anbi1d 686 . . . 4  |-  ( z  =  A  ->  (
( z  =  <. x ,  y >.  /\  ph ) 
<->  ( A  =  <. x ,  y >.  /\  ph ) ) )
982exbidv 1635 . . 3  |-  ( z  =  A  ->  ( E. x E. y ( z  =  <. x ,  y >.  /\  ph ) 
<->  E. x E. y
( A  =  <. x ,  y >.  /\  ph ) ) )
10 df-opab 4209 . . 3  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
119, 10elab2g 3028 . 2  |-  ( A  e.  _V  ->  ( A  e.  { <. x ,  y >.  |  ph } 
<->  E. x E. y
( A  =  <. x ,  y >.  /\  ph ) ) )
121, 6, 11pm5.21nii 343 1  |-  ( A  e.  { <. x ,  y >.  |  ph } 
<->  E. x E. y
( A  =  <. x ,  y >.  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1717   _Vcvv 2900   <.cop 3761   {copab 4207
This theorem is referenced by:  opelopabsbOLD  4405  opelopabsb  4407  opelopabt  4409  opelopabga  4410  opabn0  4427  iunopab  4428  epelg  4437  elxp  4836  elcnv  4990  dfmpt3  5508  opabex3d  5929  opabex3  5930  0neqopab  6059  elopaba  6349  fsplit  6391  isfunc  13989  qqhval2  24166  rtrclreclem.trans  24926  pellexlem5  26588  pellex  26590  opelopab4  27982  dicelval3  31296
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pr 4345
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-opab 4209
  Copyright terms: Public domain W3C validator