Theorem brel 4676

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 4045	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4655	. 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 3129   class class class wbr 4001   X. cxp 4622

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 4119  ax-pow 4172  ax-pr 4207

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-br 4002  df-opab 4063  df-xp 4630

This theorem is referenced by:  brab2a  4677  brab2ga  4699  soirri  5020  sotri  5021  sotri2  5023  sotri3  5024  swoer  6558  ecopovsym  6626  ecopovtrn  6627  ecopovsymg  6629  ecopovtrng  6630  ltanqi  7396  ltmnqi  7397  ltexnqi  7403  ltbtwnnqq  7409  ltbtwnnq  7410  ltrnqi  7415  prcdnql  7478  prcunqu  7479  prnmaxl  7482  prnminu  7483  prloc  7485  prarloclemcalc  7496  genplt2i  7504  genpcdl  7513  genpcuu  7514  addnqprllem  7521  addnqprulem  7522  addlocprlemlt  7525  addlocprlemeq  7527  addlocprlemgt  7528  addlocprlem  7529  nqprxx  7540  ltnqex  7543  gtnqex  7544  addnqprlemrl  7551  addnqprlemru  7552  addnqprlemfl  7553  addnqprlemfu  7554  appdivnq  7557  prmuloclemcalc  7559  prmuloc  7560  mulnqprlemrl  7567  mulnqprlemru  7568  mulnqprlemfl  7569  mulnqprlemfu  7570  ltprordil  7583  1idprl  7584  1idpru  7585  ltnqpri  7588  ltexprlemm  7594  ltexprlemopl  7595  ltexprlemlol  7596  ltexprlemopu  7597  ltexprlemupu  7598  ltexprlemdisj  7600  ltexprlemloc  7601  ltexprlemfl  7603  ltexprlemrl  7604  ltexprlemfu  7605  ltexprlemru  7606  ltexpri  7607  lteupri  7611  ltaprlem  7612  recexprlemell  7616  recexprlemelu  7617  recexprlemloc  7625  recexprlempr  7626  recexprlem1ssl  7627  recexprlem1ssu  7628  recexprlemss1l  7629  recexprlemss1u  7630  cauappcvgprlemm  7639  cauappcvgprlemlol  7641  cauappcvgprlemupu  7643  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  caucvgprlemk  7659  caucvgprlemm  7662  caucvgprlemlol  7664  caucvgprlemupu  7666  caucvgprlemladdfu  7671  caucvgprlem1  7673  caucvgprlem2  7674  caucvgprprlemk  7677  caucvgprprlemloccalc  7678  caucvgprprlemval  7682  caucvgprprlemml  7688  caucvgprprlemlol  7692  caucvgprprlemupu  7694  caucvgprprlemloc  7697  caucvgprprlem1  7703  caucvgprprlem2  7704  suplocexprlemss  7709  suplocexprlemrl  7711  suplocexprlemru  7713  suplocexprlemlub  7718  gt0srpr  7742  recexgt0sr  7767  addgt0sr  7769  mulgt0sr  7772  caucvgsrlemasr  7784  map2psrprg  7799  suplocsrlem  7802  suplocsr  7803  ltresr  7833  ltrenn  7849  dvdszrcl  11790