Theorem brel 4778

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202   ⊆ wss 3200   class class class wbr 4088   × cxp 4723

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 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-opab 4151  df-xp 4731

This theorem is referenced by:  brab2a  4779  brab2ga  4801  soirri  5131  sotri  5132  sotri2  5134  sotri3  5135  swoer  6730  ecopovsym  6800  ecopovtrn  6801  ecopovsymg  6803  ecopovtrng  6804  ltanqi  7622  ltmnqi  7623  ltexnqi  7629  ltbtwnnqq  7635  ltbtwnnq  7636  ltrnqi  7641  prcdnql  7704  prcunqu  7705  prnmaxl  7708  prnminu  7709  prloc  7711  prarloclemcalc  7722  genplt2i  7730  genpcdl  7739  genpcuu  7740  addnqprllem  7747  addnqprulem  7748  addlocprlemlt  7751  addlocprlemeq  7753  addlocprlemgt  7754  addlocprlem  7755  nqprxx  7766  ltnqex  7769  gtnqex  7770  addnqprlemrl  7777  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  appdivnq  7783  prmuloclemcalc  7785  prmuloc  7786  mulnqprlemrl  7793  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  ltprordil  7809  1idprl  7810  1idpru  7811  ltnqpri  7814  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  ltexpri  7833  lteupri  7837  ltaprlem  7838  recexprlemell  7842  recexprlemelu  7843  recexprlemloc  7851  recexprlempr  7852  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemm  7865  cauappcvgprlemlol  7867  cauappcvgprlemupu  7869  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemk  7885  caucvgprlemm  7888  caucvgprlemlol  7890  caucvgprlemupu  7892  caucvgprlemladdfu  7897  caucvgprlem1  7899  caucvgprlem2  7900  caucvgprprlemk  7903  caucvgprprlemloccalc  7904  caucvgprprlemval  7908  caucvgprprlemml  7914  caucvgprprlemlol  7918  caucvgprprlemupu  7920  caucvgprprlemloc  7923  caucvgprprlem1  7929  caucvgprprlem2  7930  suplocexprlemss  7935  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemlub  7944  gt0srpr  7968  recexgt0sr  7993  addgt0sr  7995  mulgt0sr  7998  caucvgsrlemasr  8010  map2psrprg  8025  suplocsrlem  8028  suplocsr  8029  ltresr  8059  ltrenn  8075  dvdszrcl  12355