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

Theorem brel 4392
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 3806 . 2 (𝐴𝑅𝐵𝐴(𝐶 × 𝐷)𝐵)
3 brxp 4375 . 2 (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐷))
42, 3sylib 127 1 (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  wss 2917   class class class wbr 3764   × cxp 4343
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765  df-opab 3819  df-xp 4351
This theorem is referenced by:  brab2a  4393  brab2ga  4415  soirri  4719  sotri  4720  sotri2  4722  sotri3  4723  swoer  6134  ecopovsym  6202  ecopovtrn  6203  ecopovsymg  6205  ecopovtrng  6206  ltanqi  6498  ltmnqi  6499  ltexnqi  6505  ltbtwnnqq  6511  ltbtwnnq  6512  ltrnqi  6517  prcdnql  6580  prcunqu  6581  prnmaxl  6584  prnminu  6585  prloc  6587  prarloclemcalc  6598  genplt2i  6606  genpcdl  6615  genpcuu  6616  addnqprllem  6623  addnqprulem  6624  addlocprlemlt  6627  addlocprlemeq  6629  addlocprlemgt  6630  addlocprlem  6631  nqprxx  6642  ltnqex  6645  gtnqex  6646  addnqprlemrl  6653  addnqprlemru  6654  addnqprlemfl  6655  addnqprlemfu  6656  appdivnq  6659  prmuloclemcalc  6661  prmuloc  6662  mulnqprlemrl  6669  mulnqprlemru  6670  mulnqprlemfl  6671  mulnqprlemfu  6672  ltprordil  6685  1idprl  6686  1idpru  6687  ltnqpri  6690  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemlol  6698  ltexprlemopu  6699  ltexprlemupu  6700  ltexprlemdisj  6702  ltexprlemloc  6703  ltexprlemfl  6705  ltexprlemrl  6706  ltexprlemfu  6707  ltexprlemru  6708  ltexpri  6709  lteupri  6713  ltaprlem  6714  recexprlemell  6718  recexprlemelu  6719  recexprlemloc  6727  recexprlempr  6728  recexprlem1ssl  6729  recexprlem1ssu  6730  recexprlemss1l  6731  recexprlemss1u  6732  cauappcvgprlemm  6741  cauappcvgprlemlol  6743  cauappcvgprlemupu  6745  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  caucvgprlemk  6761  caucvgprlemm  6764  caucvgprlemlol  6766  caucvgprlemupu  6768  caucvgprlemladdfu  6773  caucvgprlem1  6775  caucvgprlem2  6776  caucvgprprlemk  6779  caucvgprprlemloccalc  6780  caucvgprprlemval  6784  caucvgprprlemml  6790  caucvgprprlemlol  6794  caucvgprprlemupu  6796  caucvgprprlemloc  6799  caucvgprprlem1  6805  caucvgprprlem2  6806  gt0srpr  6831  recexgt0sr  6856  addgt0sr  6858  mulgt0sr  6860  caucvgsrlemasr  6872  ltresr  6913  ltrenn  6929
  Copyright terms: Public domain W3C validator