Theorem brel 4392

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

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1393   C_ wss 2917   class class class wbr 3764   X. cxp 4343

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765  df-opab 3819  df-xp 4351

This theorem is referenced by:  brab2a  4393  brab2ga  4415  soirri  4719  sotri  4720  sotri2  4722  sotri3  4723  swoer  6134  ecopovsym  6202  ecopovtrn  6203  ecopovsymg  6205  ecopovtrng  6206  ltanqi  6500  ltmnqi  6501  ltexnqi  6507  ltbtwnnqq  6513  ltbtwnnq  6514  ltrnqi  6519  prcdnql  6582  prcunqu  6583  prnmaxl  6586  prnminu  6587  prloc  6589  prarloclemcalc  6600  genplt2i  6608  genpcdl  6617  genpcuu  6618  addnqprllem  6625  addnqprulem  6626  addlocprlemlt  6629  addlocprlemeq  6631  addlocprlemgt  6632  addlocprlem  6633  nqprxx  6644  ltnqex  6647  gtnqex  6648  addnqprlemrl  6655  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  appdivnq  6661  prmuloclemcalc  6663  prmuloc  6664  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  ltprordil  6687  1idprl  6688  1idpru  6689  ltnqpri  6692  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  ltexpri  6711  lteupri  6715  ltaprlem  6716  recexprlemell  6720  recexprlemelu  6721  recexprlemloc  6729  recexprlempr  6730  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemm  6743  cauappcvgprlemlol  6745  cauappcvgprlemupu  6747  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemk  6763  caucvgprlemm  6766  caucvgprlemlol  6768  caucvgprlemupu  6770  caucvgprlemladdfu  6775  caucvgprlem1  6777  caucvgprlem2  6778  caucvgprprlemk  6781  caucvgprprlemloccalc  6782  caucvgprprlemval  6786  caucvgprprlemml  6792  caucvgprprlemlol  6796  caucvgprprlemupu  6798  caucvgprprlemloc  6801  caucvgprprlem1  6807  caucvgprprlem2  6808  gt0srpr  6833  recexgt0sr  6858  addgt0sr  6860  mulgt0sr  6862  caucvgsrlemasr  6874  ltresr  6915  ltrenn  6931