Theorem brel 4731

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177   ⊆ wss 3167   class class class wbr 4047   × cxp 4677

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-pr 4257

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-br 4048  df-opab 4110  df-xp 4685

This theorem is referenced by:  brab2a  4732  brab2ga  4754  soirri  5082  sotri  5083  sotri2  5085  sotri3  5086  swoer  6655  ecopovsym  6725  ecopovtrn  6726  ecopovsymg  6728  ecopovtrng  6729  ltanqi  7522  ltmnqi  7523  ltexnqi  7529  ltbtwnnqq  7535  ltbtwnnq  7536  ltrnqi  7541  prcdnql  7604  prcunqu  7605  prnmaxl  7608  prnminu  7609  prloc  7611  prarloclemcalc  7622  genplt2i  7630  genpcdl  7639  genpcuu  7640  addnqprllem  7647  addnqprulem  7648  addlocprlemlt  7651  addlocprlemeq  7653  addlocprlemgt  7654  addlocprlem  7655  nqprxx  7666  ltnqex  7669  gtnqex  7670  addnqprlemrl  7677  addnqprlemru  7678  addnqprlemfl  7679  addnqprlemfu  7680  appdivnq  7683  prmuloclemcalc  7685  prmuloc  7686  mulnqprlemrl  7693  mulnqprlemru  7694  mulnqprlemfl  7695  mulnqprlemfu  7696  ltprordil  7709  1idprl  7710  1idpru  7711  ltnqpri  7714  ltexprlemm  7720  ltexprlemopl  7721  ltexprlemlol  7722  ltexprlemopu  7723  ltexprlemupu  7724  ltexprlemdisj  7726  ltexprlemloc  7727  ltexprlemfl  7729  ltexprlemrl  7730  ltexprlemfu  7731  ltexprlemru  7732  ltexpri  7733  lteupri  7737  ltaprlem  7738  recexprlemell  7742  recexprlemelu  7743  recexprlemloc  7751  recexprlempr  7752  recexprlem1ssl  7753  recexprlem1ssu  7754  recexprlemss1l  7755  recexprlemss1u  7756  cauappcvgprlemm  7765  cauappcvgprlemlol  7767  cauappcvgprlemupu  7769  cauappcvgprlemladdfu  7774  cauappcvgprlemladdfl  7775  caucvgprlemk  7785  caucvgprlemm  7788  caucvgprlemlol  7790  caucvgprlemupu  7792  caucvgprlemladdfu  7797  caucvgprlem1  7799  caucvgprlem2  7800  caucvgprprlemk  7803  caucvgprprlemloccalc  7804  caucvgprprlemval  7808  caucvgprprlemml  7814  caucvgprprlemlol  7818  caucvgprprlemupu  7820  caucvgprprlemloc  7823  caucvgprprlem1  7829  caucvgprprlem2  7830  suplocexprlemss  7835  suplocexprlemrl  7837  suplocexprlemru  7839  suplocexprlemlub  7844  gt0srpr  7868  recexgt0sr  7893  addgt0sr  7895  mulgt0sr  7898  caucvgsrlemasr  7910  map2psrprg  7925  suplocsrlem  7928  suplocsr  7929  ltresr  7959  ltrenn  7975  dvdszrcl  12147