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

Theorem brel 4737
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 4065 . 2  |-  ( A R B  ->  A
( C  X.  D
) B )
3 brxp 4720 . 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 1684    C_ wss 3152   class class class wbr 4023    X. cxp 4687
This theorem is referenced by:  brab2a  4738  brab2ga  4763  soirri  5069  sotri  5070  sotri2  5072  sotri3  5073  soirriOLD  5074  sotriOLD  5075  ndmovord  6010  ndmovordi  6011  swoer  6688  brecop2  6752  ecopovsym  6760  ecopovtrn  6761  hartogslem1  7257  nlt1pi  8530  indpi  8531  nqerf  8554  ordpipq  8566  lterpq  8594  ltexnq  8599  ltbtwnnq  8602  ltrnq  8603  prnmadd  8621  genpcd  8630  nqpr  8638  1idpr  8653  ltexprlem4  8663  ltexpri  8667  ltaprlem  8668  prlem936  8671  reclem2pr  8672  reclem3pr  8673  reclem4pr  8674  suplem1pr  8676  suplem2pr  8677  supexpr  8678  recexsrlem  8725  addgt0sr  8726  mulgt0sr  8727  mappsrpr  8730  map2psrpr  8732  supsrlem  8733  supsr  8734  ltresr  8762  dfle2  10481  dflt2  10482  dvdszrcl  12536  letsr  14349  hmphtop  17469  vcex  21136  brtxp2  24421  brpprod3a  24426  mlteqer  25617
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-br 4024  df-opab 4078  df-xp 4695
  Copyright terms: Public domain W3C validator