Theorem brel 4822

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 4170	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4800	. 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 2209   C_ wss 3220   class class class wbr 4125   X. cxp 4767

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-pr 4341

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126  df-opab 4188  df-xp 4775

This theorem is referenced by:  brab2a  4823  brab2ga  4845  soirri  5177  sotri  5178  sotri2  5180  sotri3  5181  swoer  6825  ecopovsym  6895  ecopovtrn  6896  ecopovsymg  6898  ecopovtrng  6899  ltanqi  7759  ltmnqi  7760  ltexnqi  7766  ltbtwnnqq  7772  ltbtwnnq  7773  ltrnqi  7778  prcdnql  7841  prcunqu  7842  prnmaxl  7845  prnminu  7846  prloc  7848  prarloclemcalc  7859  genplt2i  7867  genpcdl  7876  genpcuu  7877  addnqprllem  7884  addnqprulem  7885  addlocprlemlt  7888  addlocprlemeq  7890  addlocprlemgt  7891  addlocprlem  7892  nqprxx  7903  ltnqex  7906  gtnqex  7907  addnqprlemrl  7914  addnqprlemru  7915  addnqprlemfl  7916  addnqprlemfu  7917  appdivnq  7920  prmuloclemcalc  7922  prmuloc  7923  mulnqprlemrl  7930  mulnqprlemru  7931  mulnqprlemfl  7932  mulnqprlemfu  7933  ltprordil  7946  1idprl  7947  1idpru  7948  ltnqpri  7951  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemlol  7959  ltexprlemopu  7960  ltexprlemupu  7961  ltexprlemdisj  7963  ltexprlemloc  7964  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  ltexpri  7970  lteupri  7974  ltaprlem  7975  recexprlemell  7979  recexprlemelu  7980  recexprlemloc  7988  recexprlempr  7989  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1l  7992  recexprlemss1u  7993  cauappcvgprlemm  8002  cauappcvgprlemlol  8004  cauappcvgprlemupu  8006  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  caucvgprlemk  8022  caucvgprlemm  8025  caucvgprlemlol  8027  caucvgprlemupu  8029  caucvgprlemladdfu  8034  caucvgprlem1  8036  caucvgprlem2  8037  caucvgprprlemk  8040  caucvgprprlemloccalc  8041  caucvgprprlemval  8045  caucvgprprlemml  8051  caucvgprprlemlol  8055  caucvgprprlemupu  8057  caucvgprprlemloc  8060  caucvgprprlem1  8066  caucvgprprlem2  8067  suplocexprlemss  8072  suplocexprlemrl  8074  suplocexprlemru  8076  suplocexprlemlub  8081  gt0srpr  8105  recexgt0sr  8130  addgt0sr  8132  mulgt0sr  8135  caucvgsrlemasr  8147  map2psrprg  8162  suplocsrlem  8165  suplocsr  8166  ltresr  8196  ltrenn  8212  dvdszrcl  12537