Theorem brel 4770

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 4127	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4749	. 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 3197   class class class wbr 4082   X. cxp 4716

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 4201  ax-pow 4257  ax-pr 4292

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083  df-opab 4145  df-xp 4724

This theorem is referenced by:  brab2a  4771  brab2ga  4793  soirri  5122  sotri  5123  sotri2  5125  sotri3  5126  swoer  6706  ecopovsym  6776  ecopovtrn  6777  ecopovsymg  6779  ecopovtrng  6780  ltanqi  7585  ltmnqi  7586  ltexnqi  7592  ltbtwnnqq  7598  ltbtwnnq  7599  ltrnqi  7604  prcdnql  7667  prcunqu  7668  prnmaxl  7671  prnminu  7672  prloc  7674  prarloclemcalc  7685  genplt2i  7693  genpcdl  7702  genpcuu  7703  addnqprllem  7710  addnqprulem  7711  addlocprlemlt  7714  addlocprlemeq  7716  addlocprlemgt  7717  addlocprlem  7718  nqprxx  7729  ltnqex  7732  gtnqex  7733  addnqprlemrl  7740  addnqprlemru  7741  addnqprlemfl  7742  addnqprlemfu  7743  appdivnq  7746  prmuloclemcalc  7748  prmuloc  7749  mulnqprlemrl  7756  mulnqprlemru  7757  mulnqprlemfl  7758  mulnqprlemfu  7759  ltprordil  7772  1idprl  7773  1idpru  7774  ltnqpri  7777  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemfl  7792  ltexprlemrl  7793  ltexprlemfu  7794  ltexprlemru  7795  ltexpri  7796  lteupri  7800  ltaprlem  7801  recexprlemell  7805  recexprlemelu  7806  recexprlemloc  7814  recexprlempr  7815  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1l  7818  recexprlemss1u  7819  cauappcvgprlemm  7828  cauappcvgprlemlol  7830  cauappcvgprlemupu  7832  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  caucvgprlemk  7848  caucvgprlemm  7851  caucvgprlemlol  7853  caucvgprlemupu  7855  caucvgprlemladdfu  7860  caucvgprlem1  7862  caucvgprlem2  7863  caucvgprprlemk  7866  caucvgprprlemloccalc  7867  caucvgprprlemval  7871  caucvgprprlemml  7877  caucvgprprlemlol  7881  caucvgprprlemupu  7883  caucvgprprlemloc  7886  caucvgprprlem1  7892  caucvgprprlem2  7893  suplocexprlemss  7898  suplocexprlemrl  7900  suplocexprlemru  7902  suplocexprlemlub  7907  gt0srpr  7931  recexgt0sr  7956  addgt0sr  7958  mulgt0sr  7961  caucvgsrlemasr  7973  map2psrprg  7988  suplocsrlem  7991  suplocsr  7992  ltresr  8022  ltrenn  8038  dvdszrcl  12298