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

Theorem brel 5158
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 4688 . 2 (𝐴𝑅𝐵𝐴(𝐶 × 𝐷)𝐵)
3 brxp 5137 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
42, 3sylib 208 1 (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1988  wss 3567   class class class wbr 4644   × cxp 5102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110
This theorem is referenced by:  brab2a  5184  soirri  5510  sotri  5511  sotri2  5513  sotri3  5514  ndmovord  6809  ndmovordi  6810  swoer  7757  brecop2  7826  ecopovsym  7834  ecopovtrn  7835  hartogslem1  8432  nlt1pi  9713  indpi  9714  nqerf  9737  ordpipq  9749  lterpq  9777  ltexnq  9782  ltbtwnnq  9785  ltrnq  9786  prnmadd  9804  genpcd  9813  nqpr  9821  1idpr  9836  ltexprlem4  9846  ltexpri  9850  ltaprlem  9851  prlem936  9854  reclem2pr  9855  reclem3pr  9856  reclem4pr  9857  suplem1pr  9859  suplem2pr  9860  supexpr  9861  recexsrlem  9909  addgt0sr  9910  mulgt0sr  9911  mappsrpr  9914  map2psrpr  9916  supsrlem  9917  supsr  9918  ltresr  9946  dfle2  11965  dflt2  11966  dvdszrcl  14969  letsr  17208  hmphtop  21562  vcex  27403  brtxp2  31963  brpprod3a  31968
  Copyright terms: Public domain W3C validator