Theorem brel 4727

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 4088	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4706	. 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 2176   C_ wss 3166   class class class wbr 4044   X. cxp 4673

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045  df-opab 4106  df-xp 4681

This theorem is referenced by:  brab2a  4728  brab2ga  4750  soirri  5077  sotri  5078  sotri2  5080  sotri3  5081  swoer  6648  ecopovsym  6718  ecopovtrn  6719  ecopovsymg  6721  ecopovtrng  6722  ltanqi  7515  ltmnqi  7516  ltexnqi  7522  ltbtwnnqq  7528  ltbtwnnq  7529  ltrnqi  7534  prcdnql  7597  prcunqu  7598  prnmaxl  7601  prnminu  7602  prloc  7604  prarloclemcalc  7615  genplt2i  7623  genpcdl  7632  genpcuu  7633  addnqprllem  7640  addnqprulem  7641  addlocprlemlt  7644  addlocprlemeq  7646  addlocprlemgt  7647  addlocprlem  7648  nqprxx  7659  ltnqex  7662  gtnqex  7663  addnqprlemrl  7670  addnqprlemru  7671  addnqprlemfl  7672  addnqprlemfu  7673  appdivnq  7676  prmuloclemcalc  7678  prmuloc  7679  mulnqprlemrl  7686  mulnqprlemru  7687  mulnqprlemfl  7688  mulnqprlemfu  7689  ltprordil  7702  1idprl  7703  1idpru  7704  ltnqpri  7707  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  ltexpri  7726  lteupri  7730  ltaprlem  7731  recexprlemell  7735  recexprlemelu  7736  recexprlemloc  7744  recexprlempr  7745  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  recexprlemss1u  7749  cauappcvgprlemm  7758  cauappcvgprlemlol  7760  cauappcvgprlemupu  7762  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  caucvgprlemk  7778  caucvgprlemm  7781  caucvgprlemlol  7783  caucvgprlemupu  7785  caucvgprlemladdfu  7790  caucvgprlem1  7792  caucvgprlem2  7793  caucvgprprlemk  7796  caucvgprprlemloccalc  7797  caucvgprprlemval  7801  caucvgprprlemml  7807  caucvgprprlemlol  7811  caucvgprprlemupu  7813  caucvgprprlemloc  7816  caucvgprprlem1  7822  caucvgprprlem2  7823  suplocexprlemss  7828  suplocexprlemrl  7830  suplocexprlemru  7832  suplocexprlemlub  7837  gt0srpr  7861  recexgt0sr  7886  addgt0sr  7888  mulgt0sr  7891  caucvgsrlemasr  7903  map2psrprg  7918  suplocsrlem  7921  suplocsr  7922  ltresr  7952  ltrenn  7968  dvdszrcl  12103