Theorem brel 4680

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148   ⊆ wss 3131   class class class wbr 4005   × cxp 4626

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006  df-opab 4067  df-xp 4634

This theorem is referenced by:  brab2a  4681  brab2ga  4703  soirri  5025  sotri  5026  sotri2  5028  sotri3  5029  swoer  6565  ecopovsym  6633  ecopovtrn  6634  ecopovsymg  6636  ecopovtrng  6637  ltanqi  7403  ltmnqi  7404  ltexnqi  7410  ltbtwnnqq  7416  ltbtwnnq  7417  ltrnqi  7422  prcdnql  7485  prcunqu  7486  prnmaxl  7489  prnminu  7490  prloc  7492  prarloclemcalc  7503  genplt2i  7511  genpcdl  7520  genpcuu  7521  addnqprllem  7528  addnqprulem  7529  addlocprlemlt  7532  addlocprlemeq  7534  addlocprlemgt  7535  addlocprlem  7536  nqprxx  7547  ltnqex  7550  gtnqex  7551  addnqprlemrl  7558  addnqprlemru  7559  addnqprlemfl  7560  addnqprlemfu  7561  appdivnq  7564  prmuloclemcalc  7566  prmuloc  7567  mulnqprlemrl  7574  mulnqprlemru  7575  mulnqprlemfl  7576  mulnqprlemfu  7577  ltprordil  7590  1idprl  7591  1idpru  7592  ltnqpri  7595  ltexprlemm  7601  ltexprlemopl  7602  ltexprlemlol  7603  ltexprlemopu  7604  ltexprlemupu  7605  ltexprlemdisj  7607  ltexprlemloc  7608  ltexprlemfl  7610  ltexprlemrl  7611  ltexprlemfu  7612  ltexprlemru  7613  ltexpri  7614  lteupri  7618  ltaprlem  7619  recexprlemell  7623  recexprlemelu  7624  recexprlemloc  7632  recexprlempr  7633  recexprlem1ssl  7634  recexprlem1ssu  7635  recexprlemss1l  7636  recexprlemss1u  7637  cauappcvgprlemm  7646  cauappcvgprlemlol  7648  cauappcvgprlemupu  7650  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  caucvgprlemk  7666  caucvgprlemm  7669  caucvgprlemlol  7671  caucvgprlemupu  7673  caucvgprlemladdfu  7678  caucvgprlem1  7680  caucvgprlem2  7681  caucvgprprlemk  7684  caucvgprprlemloccalc  7685  caucvgprprlemval  7689  caucvgprprlemml  7695  caucvgprprlemlol  7699  caucvgprprlemupu  7701  caucvgprprlemloc  7704  caucvgprprlem1  7710  caucvgprprlem2  7711  suplocexprlemss  7716  suplocexprlemrl  7718  suplocexprlemru  7720  suplocexprlemlub  7725  gt0srpr  7749  recexgt0sr  7774  addgt0sr  7776  mulgt0sr  7779  caucvgsrlemasr  7791  map2psrprg  7806  suplocsrlem  7809  suplocsr  7810  ltresr  7840  ltrenn  7856  dvdszrcl  11801