Theorem brel 4699

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 4065	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4678	. 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 2160   C_ wss 3144   class class class wbr 4021   X. cxp 4645

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 2163  ax-ext 2171  ax-sep 4139  ax-pow 4195  ax-pr 4230

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-br 4022  df-opab 4083  df-xp 4653

This theorem is referenced by:  brab2a  4700  brab2ga  4722  soirri  5044  sotri  5045  sotri2  5047  sotri3  5048  swoer  6591  ecopovsym  6661  ecopovtrn  6662  ecopovsymg  6664  ecopovtrng  6665  ltanqi  7436  ltmnqi  7437  ltexnqi  7443  ltbtwnnqq  7449  ltbtwnnq  7450  ltrnqi  7455  prcdnql  7518  prcunqu  7519  prnmaxl  7522  prnminu  7523  prloc  7525  prarloclemcalc  7536  genplt2i  7544  genpcdl  7553  genpcuu  7554  addnqprllem  7561  addnqprulem  7562  addlocprlemlt  7565  addlocprlemeq  7567  addlocprlemgt  7568  addlocprlem  7569  nqprxx  7580  ltnqex  7583  gtnqex  7584  addnqprlemrl  7591  addnqprlemru  7592  addnqprlemfl  7593  addnqprlemfu  7594  appdivnq  7597  prmuloclemcalc  7599  prmuloc  7600  mulnqprlemrl  7607  mulnqprlemru  7608  mulnqprlemfl  7609  mulnqprlemfu  7610  ltprordil  7623  1idprl  7624  1idpru  7625  ltnqpri  7628  ltexprlemm  7634  ltexprlemopl  7635  ltexprlemlol  7636  ltexprlemopu  7637  ltexprlemupu  7638  ltexprlemdisj  7640  ltexprlemloc  7641  ltexprlemfl  7643  ltexprlemrl  7644  ltexprlemfu  7645  ltexprlemru  7646  ltexpri  7647  lteupri  7651  ltaprlem  7652  recexprlemell  7656  recexprlemelu  7657  recexprlemloc  7665  recexprlempr  7666  recexprlem1ssl  7667  recexprlem1ssu  7668  recexprlemss1l  7669  recexprlemss1u  7670  cauappcvgprlemm  7679  cauappcvgprlemlol  7681  cauappcvgprlemupu  7683  cauappcvgprlemladdfu  7688  cauappcvgprlemladdfl  7689  caucvgprlemk  7699  caucvgprlemm  7702  caucvgprlemlol  7704  caucvgprlemupu  7706  caucvgprlemladdfu  7711  caucvgprlem1  7713  caucvgprlem2  7714  caucvgprprlemk  7717  caucvgprprlemloccalc  7718  caucvgprprlemval  7722  caucvgprprlemml  7728  caucvgprprlemlol  7732  caucvgprprlemupu  7734  caucvgprprlemloc  7737  caucvgprprlem1  7743  caucvgprprlem2  7744  suplocexprlemss  7749  suplocexprlemrl  7751  suplocexprlemru  7753  suplocexprlemlub  7758  gt0srpr  7782  recexgt0sr  7807  addgt0sr  7809  mulgt0sr  7812  caucvgsrlemasr  7824  map2psrprg  7839  suplocsrlem  7842  suplocsr  7843  ltresr  7873  ltrenn  7889  dvdszrcl  11840