ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  brel GIF version

Theorem brel 4448
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 3853 . 2 (𝐴𝑅𝐵𝐴(𝐶 × 𝐷)𝐵)
3 brxp 4431 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
42, 3sylib 120 1 (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1434  wss 2984   class class class wbr 3811   × cxp 4399
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 4000
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-br 3812  df-opab 3866  df-xp 4407
This theorem is referenced by:  brab2a  4449  brab2ga  4471  soirri  4781  sotri  4782  sotri2  4784  sotri3  4785  swoer  6250  ecopovsym  6318  ecopovtrn  6319  ecopovsymg  6321  ecopovtrng  6322  ltanqi  6864  ltmnqi  6865  ltexnqi  6871  ltbtwnnqq  6877  ltbtwnnq  6878  ltrnqi  6883  prcdnql  6946  prcunqu  6947  prnmaxl  6950  prnminu  6951  prloc  6953  prarloclemcalc  6964  genplt2i  6972  genpcdl  6981  genpcuu  6982  addnqprllem  6989  addnqprulem  6990  addlocprlemlt  6993  addlocprlemeq  6995  addlocprlemgt  6996  addlocprlem  6997  nqprxx  7008  ltnqex  7011  gtnqex  7012  addnqprlemrl  7019  addnqprlemru  7020  addnqprlemfl  7021  addnqprlemfu  7022  appdivnq  7025  prmuloclemcalc  7027  prmuloc  7028  mulnqprlemrl  7035  mulnqprlemru  7036  mulnqprlemfl  7037  mulnqprlemfu  7038  ltprordil  7051  1idprl  7052  1idpru  7053  ltnqpri  7056  ltexprlemm  7062  ltexprlemopl  7063  ltexprlemlol  7064  ltexprlemopu  7065  ltexprlemupu  7066  ltexprlemdisj  7068  ltexprlemloc  7069  ltexprlemfl  7071  ltexprlemrl  7072  ltexprlemfu  7073  ltexprlemru  7074  ltexpri  7075  lteupri  7079  ltaprlem  7080  recexprlemell  7084  recexprlemelu  7085  recexprlemloc  7093  recexprlempr  7094  recexprlem1ssl  7095  recexprlem1ssu  7096  recexprlemss1l  7097  recexprlemss1u  7098  cauappcvgprlemm  7107  cauappcvgprlemlol  7109  cauappcvgprlemupu  7111  cauappcvgprlemladdfu  7116  cauappcvgprlemladdfl  7117  caucvgprlemk  7127  caucvgprlemm  7130  caucvgprlemlol  7132  caucvgprlemupu  7134  caucvgprlemladdfu  7139  caucvgprlem1  7141  caucvgprlem2  7142  caucvgprprlemk  7145  caucvgprprlemloccalc  7146  caucvgprprlemval  7150  caucvgprprlemml  7156  caucvgprprlemlol  7160  caucvgprprlemupu  7162  caucvgprprlemloc  7165  caucvgprprlem1  7171  caucvgprprlem2  7172  gt0srpr  7197  recexgt0sr  7222  addgt0sr  7224  mulgt0sr  7226  caucvgsrlemasr  7238  ltresr  7279  ltrenn  7295  dvdszrcl  10581
  Copyright terms: Public domain W3C validator