Theorem brel 4712

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 4074	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4691	. 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 2164   C_ wss 3154   class class class wbr 4030   X. cxp 4658

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031  df-opab 4092  df-xp 4666

This theorem is referenced by:  brab2a  4713  brab2ga  4735  soirri  5061  sotri  5062  sotri2  5064  sotri3  5065  swoer  6617  ecopovsym  6687  ecopovtrn  6688  ecopovsymg  6690  ecopovtrng  6691  ltanqi  7464  ltmnqi  7465  ltexnqi  7471  ltbtwnnqq  7477  ltbtwnnq  7478  ltrnqi  7483  prcdnql  7546  prcunqu  7547  prnmaxl  7550  prnminu  7551  prloc  7553  prarloclemcalc  7564  genplt2i  7572  genpcdl  7581  genpcuu  7582  addnqprllem  7589  addnqprulem  7590  addlocprlemlt  7593  addlocprlemeq  7595  addlocprlemgt  7596  addlocprlem  7597  nqprxx  7608  ltnqex  7611  gtnqex  7612  addnqprlemrl  7619  addnqprlemru  7620  addnqprlemfl  7621  addnqprlemfu  7622  appdivnq  7625  prmuloclemcalc  7627  prmuloc  7628  mulnqprlemrl  7635  mulnqprlemru  7636  mulnqprlemfl  7637  mulnqprlemfu  7638  ltprordil  7651  1idprl  7652  1idpru  7653  ltnqpri  7656  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  ltexpri  7675  lteupri  7679  ltaprlem  7680  recexprlemell  7684  recexprlemelu  7685  recexprlemloc  7693  recexprlempr  7694  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  recexprlemss1u  7698  cauappcvgprlemm  7707  cauappcvgprlemlol  7709  cauappcvgprlemupu  7711  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  caucvgprlemk  7727  caucvgprlemm  7730  caucvgprlemlol  7732  caucvgprlemupu  7734  caucvgprlemladdfu  7739  caucvgprlem1  7741  caucvgprlem2  7742  caucvgprprlemk  7745  caucvgprprlemloccalc  7746  caucvgprprlemval  7750  caucvgprprlemml  7756  caucvgprprlemlol  7760  caucvgprprlemupu  7762  caucvgprprlemloc  7765  caucvgprprlem1  7771  caucvgprprlem2  7772  suplocexprlemss  7777  suplocexprlemrl  7779  suplocexprlemru  7781  suplocexprlemlub  7786  gt0srpr  7810  recexgt0sr  7835  addgt0sr  7837  mulgt0sr  7840  caucvgsrlemasr  7852  map2psrprg  7867  suplocsrlem  7870  suplocsr  7871  ltresr  7901  ltrenn  7917  dvdszrcl  11938