Theorem brel 4677

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

Step	Hyp	Ref	Expression
1		brel.1	. . 3 |- R C_ ( C X. D )
2	1	ssbri 4046	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4656	. 2 |- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )
4	2, 3	sylib 122	1 |- ( A R B -> ( A e. C /\ B e. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   C_ wss 3129   class class class wbr 4002   X. cxp 4623

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 4120  ax-pow 4173  ax-pr 4208

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 3577  df-sn 3598  df-pr 3599  df-op 3601  df-br 4003  df-opab 4064  df-xp 4631

This theorem is referenced by:  brab2a  4678  brab2ga  4700  soirri  5021  sotri  5022  sotri2  5024  sotri3  5025  swoer  6559  ecopovsym  6627  ecopovtrn  6628  ecopovsymg  6630  ecopovtrng  6631  ltanqi  7397  ltmnqi  7398  ltexnqi  7404  ltbtwnnqq  7410  ltbtwnnq  7411  ltrnqi  7416  prcdnql  7479  prcunqu  7480  prnmaxl  7483  prnminu  7484  prloc  7486  prarloclemcalc  7497  genplt2i  7505  genpcdl  7514  genpcuu  7515  addnqprllem  7522  addnqprulem  7523  addlocprlemlt  7526  addlocprlemeq  7528  addlocprlemgt  7529  addlocprlem  7530  nqprxx  7541  ltnqex  7544  gtnqex  7545  addnqprlemrl  7552  addnqprlemru  7553  addnqprlemfl  7554  addnqprlemfu  7555  appdivnq  7558  prmuloclemcalc  7560  prmuloc  7561  mulnqprlemrl  7568  mulnqprlemru  7569  mulnqprlemfl  7570  mulnqprlemfu  7571  ltprordil  7584  1idprl  7585  1idpru  7586  ltnqpri  7589  ltexprlemm  7595  ltexprlemopl  7596  ltexprlemlol  7597  ltexprlemopu  7598  ltexprlemupu  7599  ltexprlemdisj  7601  ltexprlemloc  7602  ltexprlemfl  7604  ltexprlemrl  7605  ltexprlemfu  7606  ltexprlemru  7607  ltexpri  7608  lteupri  7612  ltaprlem  7613  recexprlemell  7617  recexprlemelu  7618  recexprlemloc  7626  recexprlempr  7627  recexprlem1ssl  7628  recexprlem1ssu  7629  recexprlemss1l  7630  recexprlemss1u  7631  cauappcvgprlemm  7640  cauappcvgprlemlol  7642  cauappcvgprlemupu  7644  cauappcvgprlemladdfu  7649  cauappcvgprlemladdfl  7650  caucvgprlemk  7660  caucvgprlemm  7663  caucvgprlemlol  7665  caucvgprlemupu  7667  caucvgprlemladdfu  7672  caucvgprlem1  7674  caucvgprlem2  7675  caucvgprprlemk  7678  caucvgprprlemloccalc  7679  caucvgprprlemval  7683  caucvgprprlemml  7689  caucvgprprlemlol  7693  caucvgprprlemupu  7695  caucvgprprlemloc  7698  caucvgprprlem1  7704  caucvgprprlem2  7705  suplocexprlemss  7710  suplocexprlemrl  7712  suplocexprlemru  7714  suplocexprlemlub  7719  gt0srpr  7743  recexgt0sr  7768  addgt0sr  7770  mulgt0sr  7773  caucvgsrlemasr  7785  map2psrprg  7800  suplocsrlem  7803  suplocsr  7804  ltresr  7834  ltrenn  7850  dvdszrcl  11791