Theorem brel 4804

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205   ⊆ wss 3213   class class class wbr 4111   × cxp 4749

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112  df-opab 4174  df-xp 4757

This theorem is referenced by:  brab2a  4805  brab2ga  4827  soirri  5159  sotri  5160  sotri2  5162  sotri3  5163  swoer  6797  ecopovsym  6867  ecopovtrn  6868  ecopovsymg  6870  ecopovtrng  6871  ltanqi  7722  ltmnqi  7723  ltexnqi  7729  ltbtwnnqq  7735  ltbtwnnq  7736  ltrnqi  7741  prcdnql  7804  prcunqu  7805  prnmaxl  7808  prnminu  7809  prloc  7811  prarloclemcalc  7822  genplt2i  7830  genpcdl  7839  genpcuu  7840  addnqprllem  7847  addnqprulem  7848  addlocprlemlt  7851  addlocprlemeq  7853  addlocprlemgt  7854  addlocprlem  7855  nqprxx  7866  ltnqex  7869  gtnqex  7870  addnqprlemrl  7877  addnqprlemru  7878  addnqprlemfl  7879  addnqprlemfu  7880  appdivnq  7883  prmuloclemcalc  7885  prmuloc  7886  mulnqprlemrl  7893  mulnqprlemru  7894  mulnqprlemfl  7895  mulnqprlemfu  7896  ltprordil  7909  1idprl  7910  1idpru  7911  ltnqpri  7914  ltexprlemm  7920  ltexprlemopl  7921  ltexprlemlol  7922  ltexprlemopu  7923  ltexprlemupu  7924  ltexprlemdisj  7926  ltexprlemloc  7927  ltexprlemfl  7929  ltexprlemrl  7930  ltexprlemfu  7931  ltexprlemru  7932  ltexpri  7933  lteupri  7937  ltaprlem  7938  recexprlemell  7942  recexprlemelu  7943  recexprlemloc  7951  recexprlempr  7952  recexprlem1ssl  7953  recexprlem1ssu  7954  recexprlemss1l  7955  recexprlemss1u  7956  cauappcvgprlemm  7965  cauappcvgprlemlol  7967  cauappcvgprlemupu  7969  cauappcvgprlemladdfu  7974  cauappcvgprlemladdfl  7975  caucvgprlemk  7985  caucvgprlemm  7988  caucvgprlemlol  7990  caucvgprlemupu  7992  caucvgprlemladdfu  7997  caucvgprlem1  7999  caucvgprlem2  8000  caucvgprprlemk  8003  caucvgprprlemloccalc  8004  caucvgprprlemval  8008  caucvgprprlemml  8014  caucvgprprlemlol  8018  caucvgprprlemupu  8020  caucvgprprlemloc  8023  caucvgprprlem1  8029  caucvgprprlem2  8030  suplocexprlemss  8035  suplocexprlemrl  8037  suplocexprlemru  8039  suplocexprlemlub  8044  gt0srpr  8068  recexgt0sr  8093  addgt0sr  8095  mulgt0sr  8098  caucvgsrlemasr  8110  map2psrprg  8125  suplocsrlem  8128  suplocsr  8129  ltresr  8159  ltrenn  8175  dvdszrcl  12486