Theorem brel 4801

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203   ⊆ wss 3210   class class class wbr 4108   × cxp 4746

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 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-br 4109  df-opab 4171  df-xp 4754

This theorem is referenced by:  brab2a  4802  brab2ga  4824  soirri  5156  sotri  5157  sotri2  5159  sotri3  5160  swoer  6794  ecopovsym  6864  ecopovtrn  6865  ecopovsymg  6867  ecopovtrng  6868  ltanqi  7713  ltmnqi  7714  ltexnqi  7720  ltbtwnnqq  7726  ltbtwnnq  7727  ltrnqi  7732  prcdnql  7795  prcunqu  7796  prnmaxl  7799  prnminu  7800  prloc  7802  prarloclemcalc  7813  genplt2i  7821  genpcdl  7830  genpcuu  7831  addnqprllem  7838  addnqprulem  7839  addlocprlemlt  7842  addlocprlemeq  7844  addlocprlemgt  7845  addlocprlem  7846  nqprxx  7857  ltnqex  7860  gtnqex  7861  addnqprlemrl  7868  addnqprlemru  7869  addnqprlemfl  7870  addnqprlemfu  7871  appdivnq  7874  prmuloclemcalc  7876  prmuloc  7877  mulnqprlemrl  7884  mulnqprlemru  7885  mulnqprlemfl  7886  mulnqprlemfu  7887  ltprordil  7900  1idprl  7901  1idpru  7902  ltnqpri  7905  ltexprlemm  7911  ltexprlemopl  7912  ltexprlemlol  7913  ltexprlemopu  7914  ltexprlemupu  7915  ltexprlemdisj  7917  ltexprlemloc  7918  ltexprlemfl  7920  ltexprlemrl  7921  ltexprlemfu  7922  ltexprlemru  7923  ltexpri  7924  lteupri  7928  ltaprlem  7929  recexprlemell  7933  recexprlemelu  7934  recexprlemloc  7942  recexprlempr  7943  recexprlem1ssl  7944  recexprlem1ssu  7945  recexprlemss1l  7946  recexprlemss1u  7947  cauappcvgprlemm  7956  cauappcvgprlemlol  7958  cauappcvgprlemupu  7960  cauappcvgprlemladdfu  7965  cauappcvgprlemladdfl  7966  caucvgprlemk  7976  caucvgprlemm  7979  caucvgprlemlol  7981  caucvgprlemupu  7983  caucvgprlemladdfu  7988  caucvgprlem1  7990  caucvgprlem2  7991  caucvgprprlemk  7994  caucvgprprlemloccalc  7995  caucvgprprlemval  7999  caucvgprprlemml  8005  caucvgprprlemlol  8009  caucvgprprlemupu  8011  caucvgprprlemloc  8014  caucvgprprlem1  8020  caucvgprprlem2  8021  suplocexprlemss  8026  suplocexprlemrl  8028  suplocexprlemru  8030  suplocexprlemlub  8035  gt0srpr  8059  recexgt0sr  8084  addgt0sr  8086  mulgt0sr  8089  caucvgsrlemasr  8101  map2psrprg  8116  suplocsrlem  8119  suplocsr  8120  ltresr  8150  ltrenn  8166  dvdszrcl  12471