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

Theorem brel 5733
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 𝑅 ⊆ (𝐶 × 𝐷)
Assertion
Ref Expression
brel (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))

Proof of Theorem brel
StepHypRef Expression
1 brel.1 . . 3 𝑅 ⊆ (𝐶 × 𝐷)
21ssbri 5186 . 2 (𝐴𝑅𝐵𝐴(𝐶 × 𝐷)𝐵)
3 brxp 5717 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
42, 3sylib 217 1 (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  wss 3944   class class class wbr 5141   × cxp 5667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-xp 5675
This theorem is referenced by:  brab2a  5761  soirri  6116  sotri  6117  sotri2  6119  sotri3  6120  ndmovord  7580  ndmovordi  7581  swoer  8716  brecop2  8788  ecopovsym  8796  ecopovtrn  8797  hartogslem1  9519  nlt1pi  10883  indpi  10884  nqerf  10907  ordpipq  10919  lterpq  10947  ltexnq  10952  ltbtwnnq  10955  ltrnq  10956  prnmadd  10974  genpcd  10983  nqpr  10991  1idpr  11006  ltexprlem4  11016  ltexpri  11020  ltaprlem  11021  prlem936  11024  reclem2pr  11025  reclem3pr  11026  reclem4pr  11027  suplem1pr  11029  suplem2pr  11030  supexpr  11031  recexsrlem  11080  addgt0sr  11081  mulgt0sr  11082  mappsrpr  11085  map2psrpr  11087  supsrlem  11088  supsr  11089  ltresr  11117  dfle2  13108  dflt2  13109  dvdszrcl  16184  letsr  18528  hmphtop  23211  brtxp2  34683  brpprod3a  34688  brxrn2  37050  iccdisj2  47178  i0oii  47200  io1ii  47201
  Copyright terms: Public domain W3C validator