Theorem brel 4776

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 4131	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4754	. 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 2200   C_ wss 3198   class class class wbr 4086   X. cxp 4721

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087  df-opab 4149  df-xp 4729

This theorem is referenced by:  brab2a  4777  brab2ga  4799  soirri  5129  sotri  5130  sotri2  5132  sotri3  5133  swoer  6725  ecopovsym  6795  ecopovtrn  6796  ecopovsymg  6798  ecopovtrng  6799  ltanqi  7612  ltmnqi  7613  ltexnqi  7619  ltbtwnnqq  7625  ltbtwnnq  7626  ltrnqi  7631  prcdnql  7694  prcunqu  7695  prnmaxl  7698  prnminu  7699  prloc  7701  prarloclemcalc  7712  genplt2i  7720  genpcdl  7729  genpcuu  7730  addnqprllem  7737  addnqprulem  7738  addlocprlemlt  7741  addlocprlemeq  7743  addlocprlemgt  7744  addlocprlem  7745  nqprxx  7756  ltnqex  7759  gtnqex  7760  addnqprlemrl  7767  addnqprlemru  7768  addnqprlemfl  7769  addnqprlemfu  7770  appdivnq  7773  prmuloclemcalc  7775  prmuloc  7776  mulnqprlemrl  7783  mulnqprlemru  7784  mulnqprlemfl  7785  mulnqprlemfu  7786  ltprordil  7799  1idprl  7800  1idpru  7801  ltnqpri  7804  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  ltexpri  7823  lteupri  7827  ltaprlem  7828  recexprlemell  7832  recexprlemelu  7833  recexprlemloc  7841  recexprlempr  7842  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  recexprlemss1u  7846  cauappcvgprlemm  7855  cauappcvgprlemlol  7857  cauappcvgprlemupu  7859  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  caucvgprlemk  7875  caucvgprlemm  7878  caucvgprlemlol  7880  caucvgprlemupu  7882  caucvgprlemladdfu  7887  caucvgprlem1  7889  caucvgprlem2  7890  caucvgprprlemk  7893  caucvgprprlemloccalc  7894  caucvgprprlemval  7898  caucvgprprlemml  7904  caucvgprprlemlol  7908  caucvgprprlemupu  7910  caucvgprprlemloc  7913  caucvgprprlem1  7919  caucvgprprlem2  7920  suplocexprlemss  7925  suplocexprlemrl  7927  suplocexprlemru  7929  suplocexprlemlub  7934  gt0srpr  7958  recexgt0sr  7983  addgt0sr  7985  mulgt0sr  7988  caucvgsrlemasr  8000  map2psrprg  8015  suplocsrlem  8018  suplocsr  8019  ltresr  8049  ltrenn  8065  dvdszrcl  12343