Theorem brel 4745

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 4104	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4724	. 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 2178   C_ wss 3174   class class class wbr 4059   X. cxp 4691

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060  df-opab 4122  df-xp 4699

This theorem is referenced by:  brab2a  4746  brab2ga  4768  soirri  5096  sotri  5097  sotri2  5099  sotri3  5100  swoer  6671  ecopovsym  6741  ecopovtrn  6742  ecopovsymg  6744  ecopovtrng  6745  ltanqi  7550  ltmnqi  7551  ltexnqi  7557  ltbtwnnqq  7563  ltbtwnnq  7564  ltrnqi  7569  prcdnql  7632  prcunqu  7633  prnmaxl  7636  prnminu  7637  prloc  7639  prarloclemcalc  7650  genplt2i  7658  genpcdl  7667  genpcuu  7668  addnqprllem  7675  addnqprulem  7676  addlocprlemlt  7679  addlocprlemeq  7681  addlocprlemgt  7682  addlocprlem  7683  nqprxx  7694  ltnqex  7697  gtnqex  7698  addnqprlemrl  7705  addnqprlemru  7706  addnqprlemfl  7707  addnqprlemfu  7708  appdivnq  7711  prmuloclemcalc  7713  prmuloc  7714  mulnqprlemrl  7721  mulnqprlemru  7722  mulnqprlemfl  7723  mulnqprlemfu  7724  ltprordil  7737  1idprl  7738  1idpru  7739  ltnqpri  7742  ltexprlemm  7748  ltexprlemopl  7749  ltexprlemlol  7750  ltexprlemopu  7751  ltexprlemupu  7752  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemfl  7757  ltexprlemrl  7758  ltexprlemfu  7759  ltexprlemru  7760  ltexpri  7761  lteupri  7765  ltaprlem  7766  recexprlemell  7770  recexprlemelu  7771  recexprlemloc  7779  recexprlempr  7780  recexprlem1ssl  7781  recexprlem1ssu  7782  recexprlemss1l  7783  recexprlemss1u  7784  cauappcvgprlemm  7793  cauappcvgprlemlol  7795  cauappcvgprlemupu  7797  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  caucvgprlemk  7813  caucvgprlemm  7816  caucvgprlemlol  7818  caucvgprlemupu  7820  caucvgprlemladdfu  7825  caucvgprlem1  7827  caucvgprlem2  7828  caucvgprprlemk  7831  caucvgprprlemloccalc  7832  caucvgprprlemval  7836  caucvgprprlemml  7842  caucvgprprlemlol  7846  caucvgprprlemupu  7848  caucvgprprlemloc  7851  caucvgprprlem1  7857  caucvgprprlem2  7858  suplocexprlemss  7863  suplocexprlemrl  7865  suplocexprlemru  7867  suplocexprlemlub  7872  gt0srpr  7896  recexgt0sr  7921  addgt0sr  7923  mulgt0sr  7926  caucvgsrlemasr  7938  map2psrprg  7953  suplocsrlem  7956  suplocsr  7957  ltresr  7987  ltrenn  8003  dvdszrcl  12218