Theorem brel 5690

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3902   class class class wbr 5099   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5631

This theorem is referenced by:  brab2a  5718  soirri  6084  sotri  6085  sotri2  6087  sotri3  6088  ndmovord  7550  ndmovordi  7551  swoer  8669  brecop2  8752  ecopovsym  8760  ecopovtrn  8761  hartogslem1  9451  nlt1pi  10821  indpi  10822  nqerf  10845  ordpipq  10857  lterpq  10885  ltexnq  10890  ltbtwnnq  10893  ltrnq  10894  prnmadd  10912  genpcd  10921  nqpr  10929  1idpr  10944  ltexprlem4  10954  ltexpri  10958  ltaprlem  10959  prlem936  10962  reclem2pr  10963  reclem3pr  10964  reclem4pr  10965  suplem1pr  10967  suplem2pr  10968  supexpr  10969  recexsrlem  11018  addgt0sr  11019  mulgt0sr  11020  mappsrpr  11023  map2psrpr  11025  supsrlem  11026  supsr  11027  ltresr  11055  dfle2  13065  dflt2  13066  dvdszrcl  16188  letsr  18520  hmphtop  23726  brtxp2  36054  brpprod3a  36059  brxrn2  38556  aks6d1c1p1rcl  42399  iccdisj2  49178  i0oii  49201  io1ii  49202