Theorem brel 5715

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895   class class class wbr 5102   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656

This theorem is used by:  brab2a  5743  soirri  6119  sotri  6120  sotri2  6122  sotri3  6123  ndmovord  7611  ndmovordi  7612  swoer  8752  brecop2  8835  ecopovsym  8843  ecopovtrn  8844  hartogslem1  9539  nlt1pi  10994  indpi  10995  nqerf  11018  ordpipq  11030  lterpq  11058  ltexnq  11063  ltbtwnnq  11066  ltrnq  11067  prnmadd  11085  genpcd  11094  nqpr  11102  1idpr  11117  ltexprlem4  11127  ltexpri  11131  ltaprlem  11132  prlem936  11135  reclem2pr  11136  reclem3pr  11137  reclem4pr  11138  suplem1pr  11140  suplem2pr  11141  supexpr  11142  recexsrlem  11191  addgt0sr  11192  mulgt0sr  11193  mappsrpr  11196  map2psrpr  11198  supsrlem  11199  supsr  11200  ltresr  11228  dfle2  13279  dflt2  13280  dvdszrcl  16432  letsr  18772  hmphtop  24102  brtxp2  36735  brpprod3a  36740  brxrn2  39409  aks6d1c1p1rcl  43251  iccdisj2  50104  i0oii  50127  io1ii  50128