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

Theorem brel 5698
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 5151 . 2 (𝐴𝑅𝐵𝐴(𝐶 × 𝐷)𝐵)
3 brxp 5682 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
42, 3sylib 217 1 (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wss 3911   class class class wbr 5106   × cxp 5632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640
This theorem is referenced by:  brab2a  5726  soirri  6081  sotri  6082  sotri2  6084  sotri3  6085  ndmovord  7545  ndmovordi  7546  swoer  8681  brecop2  8753  ecopovsym  8761  ecopovtrn  8762  hartogslem1  9483  nlt1pi  10847  indpi  10848  nqerf  10871  ordpipq  10883  lterpq  10911  ltexnq  10916  ltbtwnnq  10919  ltrnq  10920  prnmadd  10938  genpcd  10947  nqpr  10955  1idpr  10970  ltexprlem4  10980  ltexpri  10984  ltaprlem  10985  prlem936  10988  reclem2pr  10989  reclem3pr  10990  reclem4pr  10991  suplem1pr  10993  suplem2pr  10994  supexpr  10995  recexsrlem  11044  addgt0sr  11045  mulgt0sr  11046  mappsrpr  11049  map2psrpr  11051  supsrlem  11052  supsr  11053  ltresr  11081  dfle2  13072  dflt2  13073  dvdszrcl  16146  letsr  18487  hmphtop  23145  brtxp2  34512  brpprod3a  34517  brxrn2  36883  iccdisj2  47016  i0oii  47038  io1ii  47039
  Copyright terms: Public domain W3C validator