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

Theorem relopabi 4811
Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)
Hypothesis
Ref Expression
relopabi.1  |-  A  =  { <. x ,  y
>.  |  ph }
Assertion
Ref Expression
relopabi  |-  Rel  A

Proof of Theorem relopabi
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 relopabi.1 . . . 4  |-  A  =  { <. x ,  y
>.  |  ph }
2 df-opab 4078 . . . 4  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
31, 2eqtri 2303 . . 3  |-  A  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
4 vex 2791 . . . . . . . 8  |-  x  e. 
_V
5 vex 2791 . . . . . . . 8  |-  y  e. 
_V
64, 5opelvv 4735 . . . . . . 7  |-  <. x ,  y >.  e.  ( _V  X.  _V )
7 eleq1 2343 . . . . . . 7  |-  ( z  =  <. x ,  y
>.  ->  ( z  e.  ( _V  X.  _V ) 
<-> 
<. x ,  y >.  e.  ( _V  X.  _V ) ) )
86, 7mpbiri 224 . . . . . 6  |-  ( z  =  <. x ,  y
>.  ->  z  e.  ( _V  X.  _V )
)
98adantr 451 . . . . 5  |-  ( ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
109exlimivv 1667 . . . 4  |-  ( E. x E. y ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
1110abssi 3248 . . 3  |-  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }  C_  ( _V  X.  _V )
123, 11eqsstri 3208 . 2  |-  A  C_  ( _V  X.  _V )
13 df-rel 4696 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
1412, 13mpbir 200 1  |-  Rel  A
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   {cab 2269   _Vcvv 2788    C_ wss 3152   <.cop 3643   {copab 4076    X. cxp 4687   Rel wrel 4694
This theorem is referenced by:  relopab  4812  reli  4813  rele  4814  relcnv  5051  cotr  5055  relco  5171  reloprab  5896  reldmoprab  5932  relrpss  6278  eqer  6693  ecopover  6762  relen  6868  reldom  6869  relwdom  7280  fpwwe2lem2  8254  fpwwe2lem3  8255  fpwwe2lem6  8257  fpwwe2lem7  8258  fpwwe2lem9  8260  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwelem  8267  fpwwe  8268  climrel  11966  rlimrel  11967  brstruct  13156  sscrel  13690  gaorber  14762  sylow2a  14930  efgrelexlema  15058  efgrelexlemb  15059  efgcpbllemb  15064  tpsexOLD  16657  2ndcctbss  17181  vitalilem1  18963  lgsquadlem1  20593  lgsquadlem2  20594  relrngo  21044  drngoi  21074  isdivrngo  21098  vcrel  21103  h2hlm  21560  hlimi  21767  relumgra  23866  mptrel  24124  vrrel  25491  fnerel  26267  refrel  26278  filnetlem3  26329  brabg2  26366  heiborlem3  26537  heiborlem4  26538  isdrngo1  26587  riscer  26619  prter1  26747  prter3  26750  rellindf  27278  reluslgra  28098  relusgra  28099  iscusgra0  28154  frisusgrapr  28172
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695  df-rel 4696
  Copyright terms: Public domain W3C validator