Theorem brel 5689

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3890   class class class wbr 5086   × cxp 5622

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 5231  ax-pr 5370

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630

This theorem is referenced by:  brab2a  5717  soirri  6083  sotri  6084  sotri2  6086  sotri3  6087  ndmovord  7550  ndmovordi  7551  swoer  8668  brecop2  8751  ecopovsym  8759  ecopovtrn  8760  hartogslem1  9450  nlt1pi  10820  indpi  10821  nqerf  10844  ordpipq  10856  lterpq  10884  ltexnq  10889  ltbtwnnq  10892  ltrnq  10893  prnmadd  10911  genpcd  10920  nqpr  10928  1idpr  10943  ltexprlem4  10953  ltexpri  10957  ltaprlem  10958  prlem936  10961  reclem2pr  10962  reclem3pr  10963  reclem4pr  10964  suplem1pr  10966  suplem2pr  10967  supexpr  10968  recexsrlem  11017  addgt0sr  11018  mulgt0sr  11019  mappsrpr  11022  map2psrpr  11024  supsrlem  11025  supsr  11026  ltresr  11054  dfle2  13089  dflt2  13090  dvdszrcl  16217  letsr  18550  hmphtop  23753  brtxp2  36077  brpprod3a  36082  brxrn2  38719  aks6d1c1p1rcl  42561  iccdisj2  49384  i0oii  49407  io1ii  49408