Theorem brel 4716

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167   ⊆ wss 3157   class class class wbr 4034   × cxp 4662

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035  df-opab 4096  df-xp 4670

This theorem is referenced by:  brab2a  4717  brab2ga  4739  soirri  5065  sotri  5066  sotri2  5068  sotri3  5069  swoer  6629  ecopovsym  6699  ecopovtrn  6700  ecopovsymg  6702  ecopovtrng  6703  ltanqi  7488  ltmnqi  7489  ltexnqi  7495  ltbtwnnqq  7501  ltbtwnnq  7502  ltrnqi  7507  prcdnql  7570  prcunqu  7571  prnmaxl  7574  prnminu  7575  prloc  7577  prarloclemcalc  7588  genplt2i  7596  genpcdl  7605  genpcuu  7606  addnqprllem  7613  addnqprulem  7614  addlocprlemlt  7617  addlocprlemeq  7619  addlocprlemgt  7620  addlocprlem  7621  nqprxx  7632  ltnqex  7635  gtnqex  7636  addnqprlemrl  7643  addnqprlemru  7644  addnqprlemfl  7645  addnqprlemfu  7646  appdivnq  7649  prmuloclemcalc  7651  prmuloc  7652  mulnqprlemrl  7659  mulnqprlemru  7660  mulnqprlemfl  7661  mulnqprlemfu  7662  ltprordil  7675  1idprl  7676  1idpru  7677  ltnqpri  7680  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  ltexpri  7699  lteupri  7703  ltaprlem  7704  recexprlemell  7708  recexprlemelu  7709  recexprlemloc  7717  recexprlempr  7718  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemm  7731  cauappcvgprlemlol  7733  cauappcvgprlemupu  7735  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  caucvgprlemk  7751  caucvgprlemm  7754  caucvgprlemlol  7756  caucvgprlemupu  7758  caucvgprlemladdfu  7763  caucvgprlem1  7765  caucvgprlem2  7766  caucvgprprlemk  7769  caucvgprprlemloccalc  7770  caucvgprprlemval  7774  caucvgprprlemml  7780  caucvgprprlemlol  7784  caucvgprprlemupu  7786  caucvgprprlemloc  7789  caucvgprprlem1  7795  caucvgprprlem2  7796  suplocexprlemss  7801  suplocexprlemrl  7803  suplocexprlemru  7805  suplocexprlemlub  7810  gt0srpr  7834  recexgt0sr  7859  addgt0sr  7861  mulgt0sr  7864  caucvgsrlemasr  7876  map2psrprg  7891  suplocsrlem  7894  suplocsr  7895  ltresr  7925  ltrenn  7941  dvdszrcl  11976