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

Theorem brel 4674
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  |-  R  C_  ( C  X.  D
)
Assertion
Ref Expression
brel  |-  ( A R B  ->  ( A  e.  C  /\  B  e.  D )
)

Proof of Theorem brel
StepHypRef Expression
1 brel.1 . . 3  |-  R  C_  ( C  X.  D
)
21ssbri 4044 . 2  |-  ( A R B  ->  A
( C  X.  D
) B )
3 brxp 4653 . 2  |-  ( A ( C  X.  D
) B  <->  ( A  e.  C  /\  B  e.  D ) )
42, 3sylib 122 1  |-  ( A R B  ->  ( A  e.  C  /\  B  e.  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    e. wcel 2148    C_ wss 3129   class class class wbr 4000    X. cxp 4620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-br 4001  df-opab 4062  df-xp 4628
This theorem is referenced by:  brab2a  4675  brab2ga  4697  soirri  5018  sotri  5019  sotri2  5021  sotri3  5022  swoer  6556  ecopovsym  6624  ecopovtrn  6625  ecopovsymg  6627  ecopovtrng  6628  ltanqi  7379  ltmnqi  7380  ltexnqi  7386  ltbtwnnqq  7392  ltbtwnnq  7393  ltrnqi  7398  prcdnql  7461  prcunqu  7462  prnmaxl  7465  prnminu  7466  prloc  7468  prarloclemcalc  7479  genplt2i  7487  genpcdl  7496  genpcuu  7497  addnqprllem  7504  addnqprulem  7505  addlocprlemlt  7508  addlocprlemeq  7510  addlocprlemgt  7511  addlocprlem  7512  nqprxx  7523  ltnqex  7526  gtnqex  7527  addnqprlemrl  7534  addnqprlemru  7535  addnqprlemfl  7536  addnqprlemfu  7537  appdivnq  7540  prmuloclemcalc  7542  prmuloc  7543  mulnqprlemrl  7550  mulnqprlemru  7551  mulnqprlemfl  7552  mulnqprlemfu  7553  ltprordil  7566  1idprl  7567  1idpru  7568  ltnqpri  7571  ltexprlemm  7577  ltexprlemopl  7578  ltexprlemlol  7579  ltexprlemopu  7580  ltexprlemupu  7581  ltexprlemdisj  7583  ltexprlemloc  7584  ltexprlemfl  7586  ltexprlemrl  7587  ltexprlemfu  7588  ltexprlemru  7589  ltexpri  7590  lteupri  7594  ltaprlem  7595  recexprlemell  7599  recexprlemelu  7600  recexprlemloc  7608  recexprlempr  7609  recexprlem1ssl  7610  recexprlem1ssu  7611  recexprlemss1l  7612  recexprlemss1u  7613  cauappcvgprlemm  7622  cauappcvgprlemlol  7624  cauappcvgprlemupu  7626  cauappcvgprlemladdfu  7631  cauappcvgprlemladdfl  7632  caucvgprlemk  7642  caucvgprlemm  7645  caucvgprlemlol  7647  caucvgprlemupu  7649  caucvgprlemladdfu  7654  caucvgprlem1  7656  caucvgprlem2  7657  caucvgprprlemk  7660  caucvgprprlemloccalc  7661  caucvgprprlemval  7665  caucvgprprlemml  7671  caucvgprprlemlol  7675  caucvgprprlemupu  7677  caucvgprprlemloc  7680  caucvgprprlem1  7686  caucvgprprlem2  7687  suplocexprlemss  7692  suplocexprlemrl  7694  suplocexprlemru  7696  suplocexprlemlub  7701  gt0srpr  7725  recexgt0sr  7750  addgt0sr  7752  mulgt0sr  7755  caucvgsrlemasr  7767  map2psrprg  7782  suplocsrlem  7785  suplocsr  7786  ltresr  7816  ltrenn  7832  dvdszrcl  11770
  Copyright terms: Public domain W3C validator