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

Theorem relopabi 4848
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 4115 . . . 4  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
31, 2eqtri 2336 . . 3  |-  A  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
4 vex 2825 . . . . . . . 8  |-  x  e. 
_V
5 vex 2825 . . . . . . . 8  |-  y  e. 
_V
64, 5opelvv 4772 . . . . . . 7  |-  <. x ,  y >.  e.  ( _V  X.  _V )
7 eleq1 2376 . . . . . . 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 1626 . . . 4  |-  ( E. x E. y ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
1110abssi 3282 . . 3  |-  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }  C_  ( _V  X.  _V )
123, 11eqsstri 3242 . 2  |-  A  C_  ( _V  X.  _V )
13 df-rel 4733 . 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 1532    = wceq 1633    e. wcel 1701   {cab 2302   _Vcvv 2822    C_ wss 3186   <.cop 3677   {copab 4113    X. cxp 4724   Rel wrel 4731
This theorem is referenced by:  relopab  4849  reli  4850  rele  4851  relcnv  5088  cotr  5092  relco  5208  reloprab  5938  reldmoprab  5974  relrpss  6320  eqer  6735  ecopover  6805  relen  6911  reldom  6912  relwdom  7325  fpwwe2lem2  8299  fpwwe2lem3  8300  fpwwe2lem6  8302  fpwwe2lem7  8303  fpwwe2lem9  8305  fpwwe2lem11  8307  fpwwe2lem12  8308  fpwwe2lem13  8309  fpwwelem  8312  fpwwe  8313  climrel  12013  rlimrel  12014  brstruct  13203  sscrel  13739  gaorber  14811  sylow2a  14979  efgrelexlema  15107  efgrelexlemb  15108  efgcpbllemb  15113  tpsexOLD  16713  2ndcctbss  17237  vitalilem1  19016  lgsquadlem1  20646  lgsquadlem2  20647  relrngo  21097  drngoi  21127  isdivrngo  21151  vcrel  21158  h2hlm  21615  hlimi  21822  relae  23765  relumgra  24150  mptrel  24509  fnerel  25416  refrel  25427  filnetlem3  25478  brabg2  25515  heiborlem3  25685  heiborlem4  25686  isdrngo1  25735  riscer  25767  prter1  25895  prter3  25898  rellindf  26426  reluhgra  27304  reluslgra  27320  relusgra  27321  iscusgra0  27403  frisusgrapr  27583
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-opab 4115  df-xp 4732  df-rel 4733
  Copyright terms: Public domain W3C validator