Theorem brel 5510

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2083   ⊆ wss 3865   class class class wbr 4968   × cxp 5448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969  df-opab 5031  df-xp 5456

This theorem is referenced by:  brab2a  5537  soirri  5869  sotri  5870  sotri2  5872  sotri3  5873  ndmovord  7201  ndmovordi  7202  swoer  8176  brecop2  8248  ecopovsym  8256  ecopovtrn  8257  hartogslem1  8859  nlt1pi  10181  indpi  10182  nqerf  10205  ordpipq  10217  lterpq  10245  ltexnq  10250  ltbtwnnq  10253  ltrnq  10254  prnmadd  10272  genpcd  10281  nqpr  10289  1idpr  10304  ltexprlem4  10314  ltexpri  10318  ltaprlem  10319  prlem936  10322  reclem2pr  10323  reclem3pr  10324  reclem4pr  10325  suplem1pr  10327  suplem2pr  10328  supexpr  10329  recexsrlem  10378  addgt0sr  10379  mulgt0sr  10380  mappsrpr  10383  map2psrpr  10385  supsrlem  10386  supsr  10387  ltresr  10415  dfle2  12394  dflt2  12395  dvdszrcl  15449  letsr  17670  hmphtop  22074  brtxp2  32953  brpprod3a  32958  brxrn2  35179