Theorem brel 4715

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 4077	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4694	. 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 2167   C_ wss 3157   class class class wbr 4033   X. cxp 4661

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034  df-opab 4095  df-xp 4669

This theorem is referenced by:  brab2a  4716  brab2ga  4738  soirri  5064  sotri  5065  sotri2  5067  sotri3  5068  swoer  6620  ecopovsym  6690  ecopovtrn  6691  ecopovsymg  6693  ecopovtrng  6694  ltanqi  7469  ltmnqi  7470  ltexnqi  7476  ltbtwnnqq  7482  ltbtwnnq  7483  ltrnqi  7488  prcdnql  7551  prcunqu  7552  prnmaxl  7555  prnminu  7556  prloc  7558  prarloclemcalc  7569  genplt2i  7577  genpcdl  7586  genpcuu  7587  addnqprllem  7594  addnqprulem  7595  addlocprlemlt  7598  addlocprlemeq  7600  addlocprlemgt  7601  addlocprlem  7602  nqprxx  7613  ltnqex  7616  gtnqex  7617  addnqprlemrl  7624  addnqprlemru  7625  addnqprlemfl  7626  addnqprlemfu  7627  appdivnq  7630  prmuloclemcalc  7632  prmuloc  7633  mulnqprlemrl  7640  mulnqprlemru  7641  mulnqprlemfl  7642  mulnqprlemfu  7643  ltprordil  7656  1idprl  7657  1idpru  7658  ltnqpri  7661  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  ltexpri  7680  lteupri  7684  ltaprlem  7685  recexprlemell  7689  recexprlemelu  7690  recexprlemloc  7698  recexprlempr  7699  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  recexprlemss1u  7703  cauappcvgprlemm  7712  cauappcvgprlemlol  7714  cauappcvgprlemupu  7716  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  caucvgprlemk  7732  caucvgprlemm  7735  caucvgprlemlol  7737  caucvgprlemupu  7739  caucvgprlemladdfu  7744  caucvgprlem1  7746  caucvgprlem2  7747  caucvgprprlemk  7750  caucvgprprlemloccalc  7751  caucvgprprlemval  7755  caucvgprprlemml  7761  caucvgprprlemlol  7765  caucvgprprlemupu  7767  caucvgprprlemloc  7770  caucvgprprlem1  7776  caucvgprprlem2  7777  suplocexprlemss  7782  suplocexprlemrl  7784  suplocexprlemru  7786  suplocexprlemlub  7791  gt0srpr  7815  recexgt0sr  7840  addgt0sr  7842  mulgt0sr  7845  caucvgsrlemasr  7857  map2psrprg  7872  suplocsrlem  7875  suplocsr  7876  ltresr  7906  ltrenn  7922  dvdszrcl  11957