Theorem brel 4780

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 4134	. 2 ⊢ (𝐴𝑅𝐵 → 𝐴(𝐶 × 𝐷)𝐵)
3		brxp 4758	. 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
4	2, 3	sylib 122	1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2201   ⊆ wss 3199   class class class wbr 4089   × cxp 4725

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-br 4090  df-opab 4152  df-xp 4733

This theorem is referenced by:  brab2a  4781  brab2ga  4803  soirri  5133  sotri  5134  sotri2  5136  sotri3  5137  swoer  6735  ecopovsym  6805  ecopovtrn  6806  ecopovsymg  6808  ecopovtrng  6809  ltanqi  7627  ltmnqi  7628  ltexnqi  7634  ltbtwnnqq  7640  ltbtwnnq  7641  ltrnqi  7646  prcdnql  7709  prcunqu  7710  prnmaxl  7713  prnminu  7714  prloc  7716  prarloclemcalc  7727  genplt2i  7735  genpcdl  7744  genpcuu  7745  addnqprllem  7752  addnqprulem  7753  addlocprlemlt  7756  addlocprlemeq  7758  addlocprlemgt  7759  addlocprlem  7760  nqprxx  7771  ltnqex  7774  gtnqex  7775  addnqprlemrl  7782  addnqprlemru  7783  addnqprlemfl  7784  addnqprlemfu  7785  appdivnq  7788  prmuloclemcalc  7790  prmuloc  7791  mulnqprlemrl  7798  mulnqprlemru  7799  mulnqprlemfl  7800  mulnqprlemfu  7801  ltprordil  7814  1idprl  7815  1idpru  7816  ltnqpri  7819  ltexprlemm  7825  ltexprlemopl  7826  ltexprlemlol  7827  ltexprlemopu  7828  ltexprlemupu  7829  ltexprlemdisj  7831  ltexprlemloc  7832  ltexprlemfl  7834  ltexprlemrl  7835  ltexprlemfu  7836  ltexprlemru  7837  ltexpri  7838  lteupri  7842  ltaprlem  7843  recexprlemell  7847  recexprlemelu  7848  recexprlemloc  7856  recexprlempr  7857  recexprlem1ssl  7858  recexprlem1ssu  7859  recexprlemss1l  7860  recexprlemss1u  7861  cauappcvgprlemm  7870  cauappcvgprlemlol  7872  cauappcvgprlemupu  7874  cauappcvgprlemladdfu  7879  cauappcvgprlemladdfl  7880  caucvgprlemk  7890  caucvgprlemm  7893  caucvgprlemlol  7895  caucvgprlemupu  7897  caucvgprlemladdfu  7902  caucvgprlem1  7904  caucvgprlem2  7905  caucvgprprlemk  7908  caucvgprprlemloccalc  7909  caucvgprprlemval  7913  caucvgprprlemml  7919  caucvgprprlemlol  7923  caucvgprprlemupu  7925  caucvgprprlemloc  7928  caucvgprprlem1  7934  caucvgprprlem2  7935  suplocexprlemss  7940  suplocexprlemrl  7942  suplocexprlemru  7944  suplocexprlemlub  7949  gt0srpr  7973  recexgt0sr  7998  addgt0sr  8000  mulgt0sr  8003  caucvgsrlemasr  8015  map2psrprg  8030  suplocsrlem  8033  suplocsr  8034  ltresr  8064  ltrenn  8080  dvdszrcl  12376