Theorem brel 4748

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2180   ⊆ wss 3177   class class class wbr 4062   × cxp 4694

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-br 4063  df-opab 4125  df-xp 4702

This theorem is referenced by:  brab2a  4749  brab2ga  4771  soirri  5099  sotri  5100  sotri2  5102  sotri3  5103  swoer  6678  ecopovsym  6748  ecopovtrn  6749  ecopovsymg  6751  ecopovtrng  6752  ltanqi  7557  ltmnqi  7558  ltexnqi  7564  ltbtwnnqq  7570  ltbtwnnq  7571  ltrnqi  7576  prcdnql  7639  prcunqu  7640  prnmaxl  7643  prnminu  7644  prloc  7646  prarloclemcalc  7657  genplt2i  7665  genpcdl  7674  genpcuu  7675  addnqprllem  7682  addnqprulem  7683  addlocprlemlt  7686  addlocprlemeq  7688  addlocprlemgt  7689  addlocprlem  7690  nqprxx  7701  ltnqex  7704  gtnqex  7705  addnqprlemrl  7712  addnqprlemru  7713  addnqprlemfl  7714  addnqprlemfu  7715  appdivnq  7718  prmuloclemcalc  7720  prmuloc  7721  mulnqprlemrl  7728  mulnqprlemru  7729  mulnqprlemfl  7730  mulnqprlemfu  7731  ltprordil  7744  1idprl  7745  1idpru  7746  ltnqpri  7749  ltexprlemm  7755  ltexprlemopl  7756  ltexprlemlol  7757  ltexprlemopu  7758  ltexprlemupu  7759  ltexprlemdisj  7761  ltexprlemloc  7762  ltexprlemfl  7764  ltexprlemrl  7765  ltexprlemfu  7766  ltexprlemru  7767  ltexpri  7768  lteupri  7772  ltaprlem  7773  recexprlemell  7777  recexprlemelu  7778  recexprlemloc  7786  recexprlempr  7787  recexprlem1ssl  7788  recexprlem1ssu  7789  recexprlemss1l  7790  recexprlemss1u  7791  cauappcvgprlemm  7800  cauappcvgprlemlol  7802  cauappcvgprlemupu  7804  cauappcvgprlemladdfu  7809  cauappcvgprlemladdfl  7810  caucvgprlemk  7820  caucvgprlemm  7823  caucvgprlemlol  7825  caucvgprlemupu  7827  caucvgprlemladdfu  7832  caucvgprlem1  7834  caucvgprlem2  7835  caucvgprprlemk  7838  caucvgprprlemloccalc  7839  caucvgprprlemval  7843  caucvgprprlemml  7849  caucvgprprlemlol  7853  caucvgprprlemupu  7855  caucvgprprlemloc  7858  caucvgprprlem1  7864  caucvgprprlem2  7865  suplocexprlemss  7870  suplocexprlemrl  7872  suplocexprlemru  7874  suplocexprlemlub  7879  gt0srpr  7903  recexgt0sr  7928  addgt0sr  7930  mulgt0sr  7933  caucvgsrlemasr  7945  map2psrprg  7960  suplocsrlem  7963  suplocsr  7964  ltresr  7994  ltrenn  8010  dvdszrcl  12269