Theorem brel 4827

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 4175	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4805	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   C_ wss 3220   class class class wbr 4130   X. cxp 4772

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131  df-opab 4193  df-xp 4780

This theorem is used by:  brab2a  4828  brab2ga  4850  soirri  5182  sotri  5183  sotri2  5185  sotri3  5186  swoer  6835  ecopovsym  6905  ecopovtrn  6906  ecopovsymg  6908  ecopovtrng  6909  ltanqi  7770  ltmnqi  7771  ltexnqi  7777  ltbtwnnqq  7783  ltbtwnnq  7784  ltrnqi  7789  prcdnql  7852  prcunqu  7853  prnmaxl  7856  prnminu  7857  prloc  7859  prarloclemcalc  7870  genplt2i  7878  genpcdl  7887  genpcuu  7888  addnqprllem  7895  addnqprulem  7896  addlocprlemlt  7899  addlocprlemeq  7901  addlocprlemgt  7902  addlocprlem  7903  nqprxx  7914  ltnqex  7917  gtnqex  7918  addnqprlemrl  7925  addnqprlemru  7926  addnqprlemfl  7927  addnqprlemfu  7928  appdivnq  7931  prmuloclemcalc  7933  prmuloc  7934  mulnqprlemrl  7941  mulnqprlemru  7942  mulnqprlemfl  7943  mulnqprlemfu  7944  ltprordil  7957  1idprl  7958  1idpru  7959  ltnqpri  7962  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  ltexpri  7981  lteupri  7985  ltaprlem  7986  recexprlemell  7990  recexprlemelu  7991  recexprlemloc  7999  recexprlempr  8000  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemm  8013  cauappcvgprlemlol  8015  cauappcvgprlemupu  8017  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  caucvgprlemk  8033  caucvgprlemm  8036  caucvgprlemlol  8038  caucvgprlemupu  8040  caucvgprlemladdfu  8045  caucvgprlem1  8047  caucvgprlem2  8048  caucvgprprlemk  8051  caucvgprprlemloccalc  8052  caucvgprprlemval  8056  caucvgprprlemml  8062  caucvgprprlemlol  8066  caucvgprprlemupu  8068  caucvgprprlemloc  8071  caucvgprprlem1  8077  caucvgprprlem2  8078  suplocexprlemss  8083  suplocexprlemrl  8085  suplocexprlemru  8087  suplocexprlemlub  8092  gt0srpr  8116  recexgt0sr  8141  addgt0sr  8143  mulgt0sr  8146  caucvgsrlemasr  8158  map2psrprg  8173  suplocsrlem  8176  suplocsr  8177  ltresr  8207  ltrenn  8223  dvdszrcl  12578