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

Theorem brel 5325
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 4849 . 2 (𝐴𝑅𝐵𝐴(𝐶 × 𝐷)𝐵)
3 brxp 5304 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
42, 3sylib 208 1 (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2139  wss 3715   class class class wbr 4804   × cxp 5264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272
This theorem is referenced by:  brab2a  5351  soirri  5680  sotri  5681  sotri2  5683  sotri3  5684  ndmovord  6990  ndmovordi  6991  swoer  7943  brecop2  8010  ecopovsym  8018  ecopovtrn  8019  hartogslem1  8614  nlt1pi  9940  indpi  9941  nqerf  9964  ordpipq  9976  lterpq  10004  ltexnq  10009  ltbtwnnq  10012  ltrnq  10013  prnmadd  10031  genpcd  10040  nqpr  10048  1idpr  10063  ltexprlem4  10073  ltexpri  10077  ltaprlem  10078  prlem936  10081  reclem2pr  10082  reclem3pr  10083  reclem4pr  10084  suplem1pr  10086  suplem2pr  10087  supexpr  10088  recexsrlem  10136  addgt0sr  10137  mulgt0sr  10138  mappsrpr  10141  map2psrpr  10143  supsrlem  10144  supsr  10145  ltresr  10173  dfle2  12193  dflt2  12194  dvdszrcl  15207  letsr  17448  hmphtop  21803  vcex  27763  brtxp2  32315  brpprod3a  32320  brxrn2  34478
  Copyright terms: Public domain W3C validator