Theorem brel 4679

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 4048	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4658	. 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 2148   C_ wss 3130   class class class wbr 4004   X. cxp 4625

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-opab 4066  df-xp 4633

This theorem is referenced by:  brab2a  4680  brab2ga  4702  soirri  5024  sotri  5025  sotri2  5027  sotri3  5028  swoer  6563  ecopovsym  6631  ecopovtrn  6632  ecopovsymg  6634  ecopovtrng  6635  ltanqi  7401  ltmnqi  7402  ltexnqi  7408  ltbtwnnqq  7414  ltbtwnnq  7415  ltrnqi  7420  prcdnql  7483  prcunqu  7484  prnmaxl  7487  prnminu  7488  prloc  7490  prarloclemcalc  7501  genplt2i  7509  genpcdl  7518  genpcuu  7519  addnqprllem  7526  addnqprulem  7527  addlocprlemlt  7530  addlocprlemeq  7532  addlocprlemgt  7533  addlocprlem  7534  nqprxx  7545  ltnqex  7548  gtnqex  7549  addnqprlemrl  7556  addnqprlemru  7557  addnqprlemfl  7558  addnqprlemfu  7559  appdivnq  7562  prmuloclemcalc  7564  prmuloc  7565  mulnqprlemrl  7572  mulnqprlemru  7573  mulnqprlemfl  7574  mulnqprlemfu  7575  ltprordil  7588  1idprl  7589  1idpru  7590  ltnqpri  7593  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  ltexpri  7612  lteupri  7616  ltaprlem  7617  recexprlemell  7621  recexprlemelu  7622  recexprlemloc  7630  recexprlempr  7631  recexprlem1ssl  7632  recexprlem1ssu  7633  recexprlemss1l  7634  recexprlemss1u  7635  cauappcvgprlemm  7644  cauappcvgprlemlol  7646  cauappcvgprlemupu  7648  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  caucvgprlemk  7664  caucvgprlemm  7667  caucvgprlemlol  7669  caucvgprlemupu  7671  caucvgprlemladdfu  7676  caucvgprlem1  7678  caucvgprlem2  7679  caucvgprprlemk  7682  caucvgprprlemloccalc  7683  caucvgprprlemval  7687  caucvgprprlemml  7693  caucvgprprlemlol  7697  caucvgprprlemupu  7699  caucvgprprlemloc  7702  caucvgprprlem1  7708  caucvgprprlem2  7709  suplocexprlemss  7714  suplocexprlemrl  7716  suplocexprlemru  7718  suplocexprlemlub  7723  gt0srpr  7747  recexgt0sr  7772  addgt0sr  7774  mulgt0sr  7777  caucvgsrlemasr  7789  map2psrprg  7804  suplocsrlem  7807  suplocsr  7808  ltresr  7838  ltrenn  7854  dvdszrcl  11799