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

Theorem relopabi 5000
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 4267 . . . 4  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
31, 2eqtri 2456 . . 3  |-  A  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
4 vex 2959 . . . . . . . 8  |-  x  e. 
_V
5 vex 2959 . . . . . . . 8  |-  y  e. 
_V
64, 5opelvv 4924 . . . . . . 7  |-  <. x ,  y >.  e.  ( _V  X.  _V )
7 eleq1 2496 . . . . . . 7  |-  ( z  =  <. x ,  y
>.  ->  ( z  e.  ( _V  X.  _V ) 
<-> 
<. x ,  y >.  e.  ( _V  X.  _V ) ) )
86, 7mpbiri 225 . . . . . 6  |-  ( z  =  <. x ,  y
>.  ->  z  e.  ( _V  X.  _V )
)
98adantr 452 . . . . 5  |-  ( ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
109exlimivv 1645 . . . 4  |-  ( E. x E. y ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
1110abssi 3418 . . 3  |-  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }  C_  ( _V  X.  _V )
123, 11eqsstri 3378 . 2  |-  A  C_  ( _V  X.  _V )
13 df-rel 4885 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
1412, 13mpbir 201 1  |-  Rel  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1550    = wceq 1652    e. wcel 1725   {cab 2422   _Vcvv 2956    C_ wss 3320   <.cop 3817   {copab 4265    X. cxp 4876   Rel wrel 4883
This theorem is referenced by:  relopab  5001  reli  5002  rele  5003  relcnv  5242  cotr  5246  relco  5368  reloprab  6122  reldmoprab  6158  relrpss  6523  eqer  6938  ecopover  7008  relen  7114  reldom  7115  relwdom  7534  fpwwe2lem2  8507  fpwwe2lem3  8508  fpwwe2lem6  8510  fpwwe2lem7  8511  fpwwe2lem9  8513  fpwwe2lem11  8515  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwelem  8520  fpwwe  8521  climrel  12286  rlimrel  12287  brstruct  13477  sscrel  14013  gaorber  15085  sylow2a  15253  efgrelexlema  15381  efgrelexlemb  15382  efgcpbllemb  15387  tpsexOLD  16984  2ndcctbss  17518  vitalilem1  19500  lgsquadlem1  21138  lgsquadlem2  21139  reluhgra  21336  relumgra  21349  reluslgra  21368  relusgra  21369  iscusgra0  21466  cusgrasize  21487  relrngo  21965  drngoi  21995  isdivrngo  22019  vcrel  22026  h2hlm  22483  hlimi  22690  relae  24591  mptrel  25392  fnerel  26347  refrel  26358  filnetlem3  26409  brabg2  26417  heiborlem3  26522  heiborlem4  26523  isdrngo1  26572  riscer  26604  prter1  26728  prter3  26731  rellindf  27255  frisusgrapr  28381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-opab 4267  df-xp 4884  df-rel 4885
  Copyright terms: Public domain W3C validator