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	⊢ 𝑅 ⊆ (𝐶 × 𝐷)

Assertion

Ref	Expression
brel	⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Proof of Theorem brel

Step	Hyp	Ref	Expression
1		brel.1	. . 3 ⊢ 𝑅 ⊆ (𝐶 × 𝐷)
2	1	ssbri 4176	. 2 ⊢ (𝐴𝑅𝐵 → 𝐴(𝐶 × 𝐷)𝐵)
3		brxp 4807	. 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
4	2, 3	sylib 122	1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209   ⊆ wss 3220   class class class wbr 4131   × 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  7776  ltmnqi  7777  ltexnqi  7783  ltbtwnnqq  7789  ltbtwnnq  7790  ltrnqi  7795  prcdnql  7858  prcunqu  7859  prnmaxl  7862  prnminu  7863  prloc  7865  prarloclemcalc  7876  genplt2i  7884  genpcdl  7893  genpcuu  7894  addnqprllem  7901  addnqprulem  7902  addlocprlemlt  7905  addlocprlemeq  7907  addlocprlemgt  7908  addlocprlem  7909  nqprxx  7920  ltnqex  7923  gtnqex  7924  addnqprlemrl  7931  addnqprlemru  7932  addnqprlemfl  7933  addnqprlemfu  7934  appdivnq  7937  prmuloclemcalc  7939  prmuloc  7940  mulnqprlemrl  7947  mulnqprlemru  7948  mulnqprlemfl  7949  mulnqprlemfu  7950  ltprordil  7963  1idprl  7964  1idpru  7965  ltnqpri  7968  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemlol  7976  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemdisj  7980  ltexprlemloc  7981  ltexprlemfl  7983  ltexprlemrl  7984  ltexprlemfu  7985  ltexprlemru  7986  ltexpri  7987  lteupri  7991  ltaprlem  7992  recexprlemell  7996  recexprlemelu  7997  recexprlemloc  8005  recexprlempr  8006  recexprlem1ssl  8007  recexprlem1ssu  8008  recexprlemss1l  8009  recexprlemss1u  8010  cauappcvgprlemm  8019  cauappcvgprlemlol  8021  cauappcvgprlemupu  8023  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  caucvgprlemk  8039  caucvgprlemm  8042  caucvgprlemlol  8044  caucvgprlemupu  8046  caucvgprlemladdfu  8051  caucvgprlem1  8053  caucvgprlem2  8054  caucvgprprlemk  8057  caucvgprprlemloccalc  8058  caucvgprprlemval  8062  caucvgprprlemml  8068  caucvgprprlemlol  8072  caucvgprprlemupu  8074  caucvgprprlemloc  8077  caucvgprprlem1  8083  caucvgprprlem2  8084  suplocexprlemss  8089  suplocexprlemrl  8091  suplocexprlemru  8093  suplocexprlemlub  8098  gt0srpr  8122  recexgt0sr  8147  addgt0sr  8149  mulgt0sr  8152  caucvgsrlemasr  8164  map2psrprg  8179  suplocsrlem  8182  suplocsr  8183  ltresr  8213  ltrenn  8229  dvdszrcl  12585