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  7769  ltmnqi  7770  ltexnqi  7776  ltbtwnnqq  7782  ltbtwnnq  7783  ltrnqi  7788  prcdnql  7851  prcunqu  7852  prnmaxl  7855  prnminu  7856  prloc  7858  prarloclemcalc  7869  genplt2i  7877  genpcdl  7886  genpcuu  7887  addnqprllem  7894  addnqprulem  7895  addlocprlemlt  7898  addlocprlemeq  7900  addlocprlemgt  7901  addlocprlem  7902  nqprxx  7913  ltnqex  7916  gtnqex  7917  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  appdivnq  7930  prmuloclemcalc  7932  prmuloc  7933  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  ltprordil  7956  1idprl  7957  1idpru  7958  ltnqpri  7961  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltexpri  7980  lteupri  7984  ltaprlem  7985  recexprlemell  7989  recexprlemelu  7990  recexprlemloc  7998  recexprlempr  7999  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemm  8012  cauappcvgprlemlol  8014  cauappcvgprlemupu  8016  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemk  8032  caucvgprlemm  8035  caucvgprlemlol  8037  caucvgprlemupu  8039  caucvgprlemladdfu  8044  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemk  8050  caucvgprprlemloccalc  8051  caucvgprprlemval  8055  caucvgprprlemml  8061  caucvgprprlemlol  8065  caucvgprprlemupu  8067  caucvgprprlemloc  8070  caucvgprprlem1  8076  caucvgprprlem2  8077  suplocexprlemss  8082  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemlub  8091  gt0srpr  8115  recexgt0sr  8140  addgt0sr  8142  mulgt0sr  8145  caucvgsrlemasr  8157  map2psrprg  8172  suplocsrlem  8175  suplocsr  8176  ltresr  8206  ltrenn  8222  dvdszrcl  12559