Theorem brel 4650

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 4020	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4629	. 2 |- ( A ( C X. D ) B <-> ( A e. C /\ B e. D ) )
4	2, 3	sylib 121	1 |- ( A R B -> ( A e. C /\ B e. D ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2135   C_ wss 3111   class class class wbr 3976   X. cxp 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2723  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977  df-opab 4038  df-xp 4604

This theorem is referenced by:  brab2a  4651  brab2ga  4673  soirri  4992  sotri  4993  sotri2  4995  sotri3  4996  swoer  6520  ecopovsym  6588  ecopovtrn  6589  ecopovsymg  6591  ecopovtrng  6592  ltanqi  7334  ltmnqi  7335  ltexnqi  7341  ltbtwnnqq  7347  ltbtwnnq  7348  ltrnqi  7353  prcdnql  7416  prcunqu  7417  prnmaxl  7420  prnminu  7421  prloc  7423  prarloclemcalc  7434  genplt2i  7442  genpcdl  7451  genpcuu  7452  addnqprllem  7459  addnqprulem  7460  addlocprlemlt  7463  addlocprlemeq  7465  addlocprlemgt  7466  addlocprlem  7467  nqprxx  7478  ltnqex  7481  gtnqex  7482  addnqprlemrl  7489  addnqprlemru  7490  addnqprlemfl  7491  addnqprlemfu  7492  appdivnq  7495  prmuloclemcalc  7497  prmuloc  7498  mulnqprlemrl  7505  mulnqprlemru  7506  mulnqprlemfl  7507  mulnqprlemfu  7508  ltprordil  7521  1idprl  7522  1idpru  7523  ltnqpri  7526  ltexprlemm  7532  ltexprlemopl  7533  ltexprlemlol  7534  ltexprlemopu  7535  ltexprlemupu  7536  ltexprlemdisj  7538  ltexprlemloc  7539  ltexprlemfl  7541  ltexprlemrl  7542  ltexprlemfu  7543  ltexprlemru  7544  ltexpri  7545  lteupri  7549  ltaprlem  7550  recexprlemell  7554  recexprlemelu  7555  recexprlemloc  7563  recexprlempr  7564  recexprlem1ssl  7565  recexprlem1ssu  7566  recexprlemss1l  7567  recexprlemss1u  7568  cauappcvgprlemm  7577  cauappcvgprlemlol  7579  cauappcvgprlemupu  7581  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  caucvgprlemk  7597  caucvgprlemm  7600  caucvgprlemlol  7602  caucvgprlemupu  7604  caucvgprlemladdfu  7609  caucvgprlem1  7611  caucvgprlem2  7612  caucvgprprlemk  7615  caucvgprprlemloccalc  7616  caucvgprprlemval  7620  caucvgprprlemml  7626  caucvgprprlemlol  7630  caucvgprprlemupu  7632  caucvgprprlemloc  7635  caucvgprprlem1  7641  caucvgprprlem2  7642  suplocexprlemss  7647  suplocexprlemrl  7649  suplocexprlemru  7651  suplocexprlemlub  7656  gt0srpr  7680  recexgt0sr  7705  addgt0sr  7707  mulgt0sr  7710  caucvgsrlemasr  7722  map2psrprg  7737  suplocsrlem  7740  suplocsr  7741  ltresr  7771  ltrenn  7787  dvdszrcl  11718