Theorem brel 4726

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 4087	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4705	. 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 2175   C_ wss 3165   class class class wbr 4043   X. cxp 4672

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044  df-opab 4105  df-xp 4680

This theorem is referenced by:  brab2a  4727  brab2ga  4749  soirri  5076  sotri  5077  sotri2  5079  sotri3  5080  swoer  6647  ecopovsym  6717  ecopovtrn  6718  ecopovsymg  6720  ecopovtrng  6721  ltanqi  7514  ltmnqi  7515  ltexnqi  7521  ltbtwnnqq  7527  ltbtwnnq  7528  ltrnqi  7533  prcdnql  7596  prcunqu  7597  prnmaxl  7600  prnminu  7601  prloc  7603  prarloclemcalc  7614  genplt2i  7622  genpcdl  7631  genpcuu  7632  addnqprllem  7639  addnqprulem  7640  addlocprlemlt  7643  addlocprlemeq  7645  addlocprlemgt  7646  addlocprlem  7647  nqprxx  7658  ltnqex  7661  gtnqex  7662  addnqprlemrl  7669  addnqprlemru  7670  addnqprlemfl  7671  addnqprlemfu  7672  appdivnq  7675  prmuloclemcalc  7677  prmuloc  7678  mulnqprlemrl  7685  mulnqprlemru  7686  mulnqprlemfl  7687  mulnqprlemfu  7688  ltprordil  7701  1idprl  7702  1idpru  7703  ltnqpri  7706  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemlol  7714  ltexprlemopu  7715  ltexprlemupu  7716  ltexprlemdisj  7718  ltexprlemloc  7719  ltexprlemfl  7721  ltexprlemrl  7722  ltexprlemfu  7723  ltexprlemru  7724  ltexpri  7725  lteupri  7729  ltaprlem  7730  recexprlemell  7734  recexprlemelu  7735  recexprlemloc  7743  recexprlempr  7744  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1l  7747  recexprlemss1u  7748  cauappcvgprlemm  7757  cauappcvgprlemlol  7759  cauappcvgprlemupu  7761  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  caucvgprlemk  7777  caucvgprlemm  7780  caucvgprlemlol  7782  caucvgprlemupu  7784  caucvgprlemladdfu  7789  caucvgprlem1  7791  caucvgprlem2  7792  caucvgprprlemk  7795  caucvgprprlemloccalc  7796  caucvgprprlemval  7800  caucvgprprlemml  7806  caucvgprprlemlol  7810  caucvgprprlemupu  7812  caucvgprprlemloc  7815  caucvgprprlem1  7821  caucvgprprlem2  7822  suplocexprlemss  7827  suplocexprlemrl  7829  suplocexprlemru  7831  suplocexprlemlub  7836  gt0srpr  7860  recexgt0sr  7885  addgt0sr  7887  mulgt0sr  7890  caucvgsrlemasr  7902  map2psrprg  7917  suplocsrlem  7920  suplocsr  7921  ltresr  7951  ltrenn  7967  dvdszrcl  12074