Theorem brel 5724

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3931   class class class wbr 5124   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665

This theorem is referenced by:  brab2a  5753  soirri  6120  sotri  6121  sotri2  6123  sotri3  6124  ndmovord  7602  ndmovordi  7603  swoer  8755  brecop2  8830  ecopovsym  8838  ecopovtrn  8839  hartogslem1  9561  nlt1pi  10925  indpi  10926  nqerf  10949  ordpipq  10961  lterpq  10989  ltexnq  10994  ltbtwnnq  10997  ltrnq  10998  prnmadd  11016  genpcd  11025  nqpr  11033  1idpr  11048  ltexprlem4  11058  ltexpri  11062  ltaprlem  11063  prlem936  11066  reclem2pr  11067  reclem3pr  11068  reclem4pr  11069  suplem1pr  11071  suplem2pr  11072  supexpr  11073  recexsrlem  11122  addgt0sr  11123  mulgt0sr  11124  mappsrpr  11127  map2psrpr  11129  supsrlem  11130  supsr  11131  ltresr  11159  dfle2  13168  dflt2  13169  dvdszrcl  16282  letsr  18608  hmphtop  23721  brtxp2  35904  brpprod3a  35909  brxrn2  38398  aks6d1c1p1rcl  42126  iccdisj2  48851  i0oii  48874  io1ii  48875