Theorem brel 4802

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 4154	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4780	. 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 2203   C_ wss 3211   class class class wbr 4109   X. cxp 4747

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110  df-opab 4172  df-xp 4755

This theorem is referenced by:  brab2a  4803  brab2ga  4825  soirri  5157  sotri  5158  sotri2  5160  sotri3  5161  swoer  6795  ecopovsym  6865  ecopovtrn  6866  ecopovsymg  6868  ecopovtrng  6869  ltanqi  7717  ltmnqi  7718  ltexnqi  7724  ltbtwnnqq  7730  ltbtwnnq  7731  ltrnqi  7736  prcdnql  7799  prcunqu  7800  prnmaxl  7803  prnminu  7804  prloc  7806  prarloclemcalc  7817  genplt2i  7825  genpcdl  7834  genpcuu  7835  addnqprllem  7842  addnqprulem  7843  addlocprlemlt  7846  addlocprlemeq  7848  addlocprlemgt  7849  addlocprlem  7850  nqprxx  7861  ltnqex  7864  gtnqex  7865  addnqprlemrl  7872  addnqprlemru  7873  addnqprlemfl  7874  addnqprlemfu  7875  appdivnq  7878  prmuloclemcalc  7880  prmuloc  7881  mulnqprlemrl  7888  mulnqprlemru  7889  mulnqprlemfl  7890  mulnqprlemfu  7891  ltprordil  7904  1idprl  7905  1idpru  7906  ltnqpri  7909  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  ltexpri  7928  lteupri  7932  ltaprlem  7933  recexprlemell  7937  recexprlemelu  7938  recexprlemloc  7946  recexprlempr  7947  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1l  7950  recexprlemss1u  7951  cauappcvgprlemm  7960  cauappcvgprlemlol  7962  cauappcvgprlemupu  7964  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  caucvgprlemk  7980  caucvgprlemm  7983  caucvgprlemlol  7985  caucvgprlemupu  7987  caucvgprlemladdfu  7992  caucvgprlem1  7994  caucvgprlem2  7995  caucvgprprlemk  7998  caucvgprprlemloccalc  7999  caucvgprprlemval  8003  caucvgprprlemml  8009  caucvgprprlemlol  8013  caucvgprprlemupu  8015  caucvgprprlemloc  8018  caucvgprprlem1  8024  caucvgprprlem2  8025  suplocexprlemss  8030  suplocexprlemrl  8032  suplocexprlemru  8034  suplocexprlemlub  8039  gt0srpr  8063  recexgt0sr  8088  addgt0sr  8090  mulgt0sr  8093  caucvgsrlemasr  8105  map2psrprg  8120  suplocsrlem  8123  suplocsr  8124  ltresr  8154  ltrenn  8170  dvdszrcl  12478