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

Theorem brel 4418
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 3835 . 2 (𝐴𝑅𝐵𝐴(𝐶 × 𝐷)𝐵)
3 brxp 4401 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
42, 3sylib 120 1 (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1434  wss 2974   class class class wbr 3793   × cxp 4369
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 2064  ax-sep 3904  ax-pow 3956  ax-pr 3972
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-pw 3392  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794  df-opab 3848  df-xp 4377
This theorem is referenced by:  brab2a  4419  brab2ga  4441  soirri  4749  sotri  4750  sotri2  4752  sotri3  4753  swoer  6200  ecopovsym  6268  ecopovtrn  6269  ecopovsymg  6271  ecopovtrng  6272  ltanqi  6654  ltmnqi  6655  ltexnqi  6661  ltbtwnnqq  6667  ltbtwnnq  6668  ltrnqi  6673  prcdnql  6736  prcunqu  6737  prnmaxl  6740  prnminu  6741  prloc  6743  prarloclemcalc  6754  genplt2i  6762  genpcdl  6771  genpcuu  6772  addnqprllem  6779  addnqprulem  6780  addlocprlemlt  6783  addlocprlemeq  6785  addlocprlemgt  6786  addlocprlem  6787  nqprxx  6798  ltnqex  6801  gtnqex  6802  addnqprlemrl  6809  addnqprlemru  6810  addnqprlemfl  6811  addnqprlemfu  6812  appdivnq  6815  prmuloclemcalc  6817  prmuloc  6818  mulnqprlemrl  6825  mulnqprlemru  6826  mulnqprlemfl  6827  mulnqprlemfu  6828  ltprordil  6841  1idprl  6842  1idpru  6843  ltnqpri  6846  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemfl  6861  ltexprlemrl  6862  ltexprlemfu  6863  ltexprlemru  6864  ltexpri  6865  lteupri  6869  ltaprlem  6870  recexprlemell  6874  recexprlemelu  6875  recexprlemloc  6883  recexprlempr  6884  recexprlem1ssl  6885  recexprlem1ssu  6886  recexprlemss1l  6887  recexprlemss1u  6888  cauappcvgprlemm  6897  cauappcvgprlemlol  6899  cauappcvgprlemupu  6901  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  caucvgprlemk  6917  caucvgprlemm  6920  caucvgprlemlol  6922  caucvgprlemupu  6924  caucvgprlemladdfu  6929  caucvgprlem1  6931  caucvgprlem2  6932  caucvgprprlemk  6935  caucvgprprlemloccalc  6936  caucvgprprlemval  6940  caucvgprprlemml  6946  caucvgprprlemlol  6950  caucvgprprlemupu  6952  caucvgprprlemloc  6955  caucvgprprlem1  6961  caucvgprprlem2  6962  gt0srpr  6987  recexgt0sr  7012  addgt0sr  7014  mulgt0sr  7016  caucvgsrlemasr  7028  ltresr  7069  ltrenn  7085  dvdszrcl  10345
  Copyright terms: Public domain W3C validator