Theorem brel 4829

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 4176	. 2 |- ( A R B -> A ( C X. D ) B )
3		brxp 4807	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   C_ wss 3220   class class class wbr 4131   X. cxp 4774

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132  df-opab 4194  df-xp 4782

This theorem is used by:  brab2a  4830  brab2ga  4852  soirri  5185  sotri  5186  sotri2  5188  sotri3  5189  swoer  6839  ecopovsym  6909  ecopovtrn  6910  ecopovsymg  6912  ecopovtrng  6913  ltanqi  7775  ltmnqi  7776  ltexnqi  7782  ltbtwnnqq  7788  ltbtwnnq  7789  ltrnqi  7794  prcdnql  7857  prcunqu  7858  prnmaxl  7861  prnminu  7862  prloc  7864  prarloclemcalc  7875  genplt2i  7883  genpcdl  7892  genpcuu  7893  addnqprllem  7900  addnqprulem  7901  addlocprlemlt  7904  addlocprlemeq  7906  addlocprlemgt  7907  addlocprlem  7908  nqprxx  7919  ltnqex  7922  gtnqex  7923  addnqprlemrl  7930  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  appdivnq  7936  prmuloclemcalc  7938  prmuloc  7939  mulnqprlemrl  7946  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  ltprordil  7962  1idprl  7963  1idpru  7964  ltnqpri  7967  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  ltexpri  7986  lteupri  7990  ltaprlem  7991  recexprlemell  7995  recexprlemelu  7996  recexprlemloc  8004  recexprlempr  8005  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemm  8018  cauappcvgprlemlol  8020  cauappcvgprlemupu  8022  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemk  8038  caucvgprlemm  8041  caucvgprlemlol  8043  caucvgprlemupu  8045  caucvgprlemladdfu  8050  caucvgprlem1  8052  caucvgprlem2  8053  caucvgprprlemk  8056  caucvgprprlemloccalc  8057  caucvgprprlemval  8061  caucvgprprlemml  8067  caucvgprprlemlol  8071  caucvgprprlemupu  8073  caucvgprprlemloc  8076  caucvgprprlem1  8082  caucvgprprlem2  8083  suplocexprlemss  8088  suplocexprlemrl  8090  suplocexprlemru  8092  suplocexprlemlub  8097  gt0srpr  8121  recexgt0sr  8146  addgt0sr  8148  mulgt0sr  8151  caucvgsrlemasr  8163  map2psrprg  8178  suplocsrlem  8181  suplocsr  8182  ltresr  8212  ltrenn  8228  dvdszrcl  12584