Theorem brel 4778

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 4133	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4756	. 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 2202   C_ wss 3200   class class class wbr 4088   X. cxp 4723

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-opab 4151  df-xp 4731

This theorem is referenced by:  brab2a  4779  brab2ga  4801  soirri  5131  sotri  5132  sotri2  5134  sotri3  5135  swoer  6729  ecopovsym  6799  ecopovtrn  6800  ecopovsymg  6802  ecopovtrng  6803  ltanqi  7621  ltmnqi  7622  ltexnqi  7628  ltbtwnnqq  7634  ltbtwnnq  7635  ltrnqi  7640  prcdnql  7703  prcunqu  7704  prnmaxl  7707  prnminu  7708  prloc  7710  prarloclemcalc  7721  genplt2i  7729  genpcdl  7738  genpcuu  7739  addnqprllem  7746  addnqprulem  7747  addlocprlemlt  7750  addlocprlemeq  7752  addlocprlemgt  7753  addlocprlem  7754  nqprxx  7765  ltnqex  7768  gtnqex  7769  addnqprlemrl  7776  addnqprlemru  7777  addnqprlemfl  7778  addnqprlemfu  7779  appdivnq  7782  prmuloclemcalc  7784  prmuloc  7785  mulnqprlemrl  7792  mulnqprlemru  7793  mulnqprlemfl  7794  mulnqprlemfu  7795  ltprordil  7808  1idprl  7809  1idpru  7810  ltnqpri  7813  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  ltexpri  7832  lteupri  7836  ltaprlem  7837  recexprlemell  7841  recexprlemelu  7842  recexprlemloc  7850  recexprlempr  7851  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemm  7864  cauappcvgprlemlol  7866  cauappcvgprlemupu  7868  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  caucvgprlemk  7884  caucvgprlemm  7887  caucvgprlemlol  7889  caucvgprlemupu  7891  caucvgprlemladdfu  7896  caucvgprlem1  7898  caucvgprlem2  7899  caucvgprprlemk  7902  caucvgprprlemloccalc  7903  caucvgprprlemval  7907  caucvgprprlemml  7913  caucvgprprlemlol  7917  caucvgprprlemupu  7919  caucvgprprlemloc  7922  caucvgprprlem1  7928  caucvgprprlem2  7929  suplocexprlemss  7934  suplocexprlemrl  7936  suplocexprlemru  7938  suplocexprlemlub  7943  gt0srpr  7967  recexgt0sr  7992  addgt0sr  7994  mulgt0sr  7997  caucvgsrlemasr  8009  map2psrprg  8024  suplocsrlem  8027  suplocsr  8028  ltresr  8058  ltrenn  8074  dvdszrcl  12352