Theorem brel 4773

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200   ⊆ wss 3197   class class class wbr 4083   × cxp 4718

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4259  ax-pr 4294

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-opab 4146  df-xp 4726

This theorem is referenced by:  brab2a  4774  brab2ga  4796  soirri  5126  sotri  5127  sotri2  5129  sotri3  5130  swoer  6721  ecopovsym  6791  ecopovtrn  6792  ecopovsymg  6794  ecopovtrng  6795  ltanqi  7605  ltmnqi  7606  ltexnqi  7612  ltbtwnnqq  7618  ltbtwnnq  7619  ltrnqi  7624  prcdnql  7687  prcunqu  7688  prnmaxl  7691  prnminu  7692  prloc  7694  prarloclemcalc  7705  genplt2i  7713  genpcdl  7722  genpcuu  7723  addnqprllem  7730  addnqprulem  7731  addlocprlemlt  7734  addlocprlemeq  7736  addlocprlemgt  7737  addlocprlem  7738  nqprxx  7749  ltnqex  7752  gtnqex  7753  addnqprlemrl  7760  addnqprlemru  7761  addnqprlemfl  7762  addnqprlemfu  7763  appdivnq  7766  prmuloclemcalc  7768  prmuloc  7769  mulnqprlemrl  7776  mulnqprlemru  7777  mulnqprlemfl  7778  mulnqprlemfu  7779  ltprordil  7792  1idprl  7793  1idpru  7794  ltnqpri  7797  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemlol  7805  ltexprlemopu  7806  ltexprlemupu  7807  ltexprlemdisj  7809  ltexprlemloc  7810  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  ltexpri  7816  lteupri  7820  ltaprlem  7821  recexprlemell  7825  recexprlemelu  7826  recexprlemloc  7834  recexprlempr  7835  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  recexprlemss1u  7839  cauappcvgprlemm  7848  cauappcvgprlemlol  7850  cauappcvgprlemupu  7852  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  caucvgprlemk  7868  caucvgprlemm  7871  caucvgprlemlol  7873  caucvgprlemupu  7875  caucvgprlemladdfu  7880  caucvgprlem1  7882  caucvgprlem2  7883  caucvgprprlemk  7886  caucvgprprlemloccalc  7887  caucvgprprlemval  7891  caucvgprprlemml  7897  caucvgprprlemlol  7901  caucvgprprlemupu  7903  caucvgprprlemloc  7906  caucvgprprlem1  7912  caucvgprprlem2  7913  suplocexprlemss  7918  suplocexprlemrl  7920  suplocexprlemru  7922  suplocexprlemlub  7927  gt0srpr  7951  recexgt0sr  7976  addgt0sr  7978  mulgt0sr  7981  caucvgsrlemasr  7993  map2psrprg  8008  suplocsrlem  8011  suplocsr  8012  ltresr  8042  ltrenn  8058  dvdszrcl  12324