Theorem brel 4529

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1448   ⊆ wss 3021   class class class wbr 3875   × cxp 4475

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-v 2643  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-br 3876  df-opab 3930  df-xp 4483

This theorem is referenced by:  brab2a  4530  brab2ga  4552  soirri  4869  sotri  4870  sotri2  4872  sotri3  4873  swoer  6387  ecopovsym  6455  ecopovtrn  6456  ecopovsymg  6458  ecopovtrng  6459  ltanqi  7111  ltmnqi  7112  ltexnqi  7118  ltbtwnnqq  7124  ltbtwnnq  7125  ltrnqi  7130  prcdnql  7193  prcunqu  7194  prnmaxl  7197  prnminu  7198  prloc  7200  prarloclemcalc  7211  genplt2i  7219  genpcdl  7228  genpcuu  7229  addnqprllem  7236  addnqprulem  7237  addlocprlemlt  7240  addlocprlemeq  7242  addlocprlemgt  7243  addlocprlem  7244  nqprxx  7255  ltnqex  7258  gtnqex  7259  addnqprlemrl  7266  addnqprlemru  7267  addnqprlemfl  7268  addnqprlemfu  7269  appdivnq  7272  prmuloclemcalc  7274  prmuloc  7275  mulnqprlemrl  7282  mulnqprlemru  7283  mulnqprlemfl  7284  mulnqprlemfu  7285  ltprordil  7298  1idprl  7299  1idpru  7300  ltnqpri  7303  ltexprlemm  7309  ltexprlemopl  7310  ltexprlemlol  7311  ltexprlemopu  7312  ltexprlemupu  7313  ltexprlemdisj  7315  ltexprlemloc  7316  ltexprlemfl  7318  ltexprlemrl  7319  ltexprlemfu  7320  ltexprlemru  7321  ltexpri  7322  lteupri  7326  ltaprlem  7327  recexprlemell  7331  recexprlemelu  7332  recexprlemloc  7340  recexprlempr  7341  recexprlem1ssl  7342  recexprlem1ssu  7343  recexprlemss1l  7344  recexprlemss1u  7345  cauappcvgprlemm  7354  cauappcvgprlemlol  7356  cauappcvgprlemupu  7358  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  caucvgprlemk  7374  caucvgprlemm  7377  caucvgprlemlol  7379  caucvgprlemupu  7381  caucvgprlemladdfu  7386  caucvgprlem1  7388  caucvgprlem2  7389  caucvgprprlemk  7392  caucvgprprlemloccalc  7393  caucvgprprlemval  7397  caucvgprprlemml  7403  caucvgprprlemlol  7407  caucvgprprlemupu  7409  caucvgprprlemloc  7412  caucvgprprlem1  7418  caucvgprprlem2  7419  gt0srpr  7444  recexgt0sr  7469  addgt0sr  7471  mulgt0sr  7473  caucvgsrlemasr  7485  ltresr  7526  ltrenn  7542  dvdszrcl  11293