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

Theorem brel 4774
Description: Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
Hypothesis
Ref Expression
brel.1  |-  R  C_  ( C  X.  D
)
Assertion
Ref Expression
brel  |-  ( A R B  ->  ( A  e.  C  /\  B  e.  D )
)

Proof of Theorem brel
StepHypRef Expression
1 brel.1 . . 3  |-  R  C_  ( C  X.  D
)
21ssbri 4102 . 2  |-  ( A R B  ->  A
( C  X.  D
) B )
3 brxp 4757 . 2  |-  ( A ( C  X.  D
) B  <->  ( A  e.  C  /\  B  e.  D ) )
42, 3sylib 188 1  |-  ( A R B  ->  ( A  e.  C  /\  B  e.  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1701    C_ wss 3186   class class class wbr 4060    X. cxp 4724
This theorem is referenced by:  brab2a  4775  brab2ga  4800  soirri  5106  sotri  5107  sotri2  5109  sotri3  5110  soirriOLD  5111  sotriOLD  5112  ndmovord  6052  ndmovordi  6053  swoer  6730  brecop2  6795  ecopovsym  6803  ecopovtrn  6804  hartogslem1  7302  nlt1pi  8575  indpi  8576  nqerf  8599  ordpipq  8611  lterpq  8639  ltexnq  8644  ltbtwnnq  8647  ltrnq  8648  prnmadd  8666  genpcd  8675  nqpr  8683  1idpr  8698  ltexprlem4  8708  ltexpri  8712  ltaprlem  8713  prlem936  8716  reclem2pr  8717  reclem3pr  8718  reclem4pr  8719  suplem1pr  8721  suplem2pr  8722  supexpr  8723  recexsrlem  8770  addgt0sr  8771  mulgt0sr  8772  mappsrpr  8775  map2psrpr  8777  supsrlem  8778  supsr  8779  ltresr  8807  dfle2  10528  dflt2  10529  dvdszrcl  12583  letsr  14398  hmphtop  17525  vcex  21191  brtxp2  24806  brpprod3a  24811
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-br 4061  df-opab 4115  df-xp 4732
  Copyright terms: Public domain W3C validator