Theorem brel 4776

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200   ⊆ wss 3198   class class class wbr 4086   × cxp 4721

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 4205  ax-pow 4262  ax-pr 4297

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087  df-opab 4149  df-xp 4729

This theorem is referenced by:  brab2a  4777  brab2ga  4799  soirri  5129  sotri  5130  sotri2  5132  sotri3  5133  swoer  6725  ecopovsym  6795  ecopovtrn  6796  ecopovsymg  6798  ecopovtrng  6799  ltanqi  7615  ltmnqi  7616  ltexnqi  7622  ltbtwnnqq  7628  ltbtwnnq  7629  ltrnqi  7634  prcdnql  7697  prcunqu  7698  prnmaxl  7701  prnminu  7702  prloc  7704  prarloclemcalc  7715  genplt2i  7723  genpcdl  7732  genpcuu  7733  addnqprllem  7740  addnqprulem  7741  addlocprlemlt  7744  addlocprlemeq  7746  addlocprlemgt  7747  addlocprlem  7748  nqprxx  7759  ltnqex  7762  gtnqex  7763  addnqprlemrl  7770  addnqprlemru  7771  addnqprlemfl  7772  addnqprlemfu  7773  appdivnq  7776  prmuloclemcalc  7778  prmuloc  7779  mulnqprlemrl  7786  mulnqprlemru  7787  mulnqprlemfl  7788  mulnqprlemfu  7789  ltprordil  7802  1idprl  7803  1idpru  7804  ltnqpri  7807  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemlol  7815  ltexprlemopu  7816  ltexprlemupu  7817  ltexprlemdisj  7819  ltexprlemloc  7820  ltexprlemfl  7822  ltexprlemrl  7823  ltexprlemfu  7824  ltexprlemru  7825  ltexpri  7826  lteupri  7830  ltaprlem  7831  recexprlemell  7835  recexprlemelu  7836  recexprlemloc  7844  recexprlempr  7845  recexprlem1ssl  7846  recexprlem1ssu  7847  recexprlemss1l  7848  recexprlemss1u  7849  cauappcvgprlemm  7858  cauappcvgprlemlol  7860  cauappcvgprlemupu  7862  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  caucvgprlemk  7878  caucvgprlemm  7881  caucvgprlemlol  7883  caucvgprlemupu  7885  caucvgprlemladdfu  7890  caucvgprlem1  7892  caucvgprlem2  7893  caucvgprprlemk  7896  caucvgprprlemloccalc  7897  caucvgprprlemval  7901  caucvgprprlemml  7907  caucvgprprlemlol  7911  caucvgprprlemupu  7913  caucvgprprlemloc  7916  caucvgprprlem1  7922  caucvgprprlem2  7923  suplocexprlemss  7928  suplocexprlemrl  7930  suplocexprlemru  7932  suplocexprlemlub  7937  gt0srpr  7961  recexgt0sr  7986  addgt0sr  7988  mulgt0sr  7991  caucvgsrlemasr  8003  map2psrprg  8018  suplocsrlem  8021  suplocsr  8022  ltresr  8052  ltrenn  8068  dvdszrcl  12346