Theorem brel 4490

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438   C_ wss 2999   class class class wbr 3845   X. cxp 4436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-br 3846  df-opab 3900  df-xp 4444

This theorem is referenced by:  brab2a  4491  brab2ga  4513  soirri  4826  sotri  4827  sotri2  4829  sotri3  4830  swoer  6320  ecopovsym  6388  ecopovtrn  6389  ecopovsymg  6391  ecopovtrng  6392  ltanqi  6961  ltmnqi  6962  ltexnqi  6968  ltbtwnnqq  6974  ltbtwnnq  6975  ltrnqi  6980  prcdnql  7043  prcunqu  7044  prnmaxl  7047  prnminu  7048  prloc  7050  prarloclemcalc  7061  genplt2i  7069  genpcdl  7078  genpcuu  7079  addnqprllem  7086  addnqprulem  7087  addlocprlemlt  7090  addlocprlemeq  7092  addlocprlemgt  7093  addlocprlem  7094  nqprxx  7105  ltnqex  7108  gtnqex  7109  addnqprlemrl  7116  addnqprlemru  7117  addnqprlemfl  7118  addnqprlemfu  7119  appdivnq  7122  prmuloclemcalc  7124  prmuloc  7125  mulnqprlemrl  7132  mulnqprlemru  7133  mulnqprlemfl  7134  mulnqprlemfu  7135  ltprordil  7148  1idprl  7149  1idpru  7150  ltnqpri  7153  ltexprlemm  7159  ltexprlemopl  7160  ltexprlemlol  7161  ltexprlemopu  7162  ltexprlemupu  7163  ltexprlemdisj  7165  ltexprlemloc  7166  ltexprlemfl  7168  ltexprlemrl  7169  ltexprlemfu  7170  ltexprlemru  7171  ltexpri  7172  lteupri  7176  ltaprlem  7177  recexprlemell  7181  recexprlemelu  7182  recexprlemloc  7190  recexprlempr  7191  recexprlem1ssl  7192  recexprlem1ssu  7193  recexprlemss1l  7194  recexprlemss1u  7195  cauappcvgprlemm  7204  cauappcvgprlemlol  7206  cauappcvgprlemupu  7208  cauappcvgprlemladdfu  7213  cauappcvgprlemladdfl  7214  caucvgprlemk  7224  caucvgprlemm  7227  caucvgprlemlol  7229  caucvgprlemupu  7231  caucvgprlemladdfu  7236  caucvgprlem1  7238  caucvgprlem2  7239  caucvgprprlemk  7242  caucvgprprlemloccalc  7243  caucvgprprlemval  7247  caucvgprprlemml  7253  caucvgprprlemlol  7257  caucvgprprlemupu  7259  caucvgprprlemloc  7262  caucvgprprlem1  7268  caucvgprprlem2  7269  gt0srpr  7294  recexgt0sr  7319  addgt0sr  7321  mulgt0sr  7323  caucvgsrlemasr  7335  ltresr  7376  ltrenn  7392  dvdszrcl  11079