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

Theorem relopabi 4961
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 4348 . . . 4  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
31, 2eqtri 2461 . . 3  |-  A  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
4 vex 2973 . . . . . . . 8  |-  x  e. 
_V
5 vex 2973 . . . . . . . 8  |-  y  e. 
_V
64, 5opelvv 4881 . . . . . . 7  |-  <. x ,  y >.  e.  ( _V  X.  _V )
7 eleq1 2501 . . . . . . 7  |-  ( z  =  <. x ,  y
>.  ->  ( z  e.  ( _V  X.  _V ) 
<-> 
<. x ,  y >.  e.  ( _V  X.  _V ) ) )
86, 7mpbiri 233 . . . . . 6  |-  ( z  =  <. x ,  y
>.  ->  z  e.  ( _V  X.  _V )
)
98adantr 462 . . . . 5  |-  ( ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
109exlimivv 1694 . . . 4  |-  ( E. x E. y ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
1110abssi 3424 . . 3  |-  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }  C_  ( _V  X.  _V )
123, 11eqsstri 3383 . 2  |-  A  C_  ( _V  X.  _V )
13 df-rel 4843 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
1412, 13mpbir 209 1  |-  Rel  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1364   E.wex 1591    e. wcel 1761   {cab 2427   _Vcvv 2970    C_ wss 3325   <.cop 3880   {copab 4346    X. cxp 4834   Rel wrel 4841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-opab 4348  df-xp 4842  df-rel 4843
This theorem is referenced by:  relopab  4962  reli  4963  rele  4964  relcnv  5203  cotr  5207  relco  5333  reloprab  6133  reldmoprab  6174  relrpss  6360  eqer  7130  ecopover  7200  relen  7311  reldom  7312  relfsupp  7618  fsuppimp  7622  wemapso2  7764  relwdom  7777  fpwwe2lem2  8795  fpwwe2lem3  8796  fpwwe2lem6  8798  fpwwe2lem7  8799  fpwwe2lem9  8801  fpwwe2lem11  8803  fpwwe2lem12  8804  fpwwe2lem13  8805  fpwwelem  8808  fpwwe  8809  climrel  12966  rlimrel  12967  brstruct  14178  sscrel  14722  gaorber  15819  sylow2a  16111  efgrelexlema  16239  efgrelexlemb  16240  efgcpbllemb  16245  rellindf  18196  tpsexOLD  18483  2ndcctbss  19018  vitalilem1  21047  lgsquadlem1  22652  lgsquadlem2  22653  reluhgra  23170  relumgra  23183  reluslgra  23202  relusgra  23203  iscusgra0  23300  cusgrasize  23321  relrngo  23799  drngoi  23829  isdivrngo  23853  vcrel  23860  h2hlm  24317  hlimi  24525  relae  26592  mptrel  27508  fnerel  28464  refrel  28475  filnetlem3  28526  brabg2  28534  heiborlem3  28637  heiborlem4  28638  isdrngo1  28687  riscer  28719  prter1  28949  prter3  28952  erclwwlkrel  30405  erclwwlknrel  30421  frisusgrapr  30508  rellininds  30818
  Copyright terms: Public domain W3C validator