Theorem brel 5754

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106   ⊆ wss 3963   class class class wbr 5148   × cxp 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695

This theorem is referenced by:  brab2a  5782  soirri  6149  sotri  6150  sotri2  6152  sotri3  6153  ndmovord  7623  ndmovordi  7624  swoer  8775  brecop2  8850  ecopovsym  8858  ecopovtrn  8859  hartogslem1  9580  nlt1pi  10944  indpi  10945  nqerf  10968  ordpipq  10980  lterpq  11008  ltexnq  11013  ltbtwnnq  11016  ltrnq  11017  prnmadd  11035  genpcd  11044  nqpr  11052  1idpr  11067  ltexprlem4  11077  ltexpri  11081  ltaprlem  11082  prlem936  11085  reclem2pr  11086  reclem3pr  11087  reclem4pr  11088  suplem1pr  11090  suplem2pr  11091  supexpr  11092  recexsrlem  11141  addgt0sr  11142  mulgt0sr  11143  mappsrpr  11146  map2psrpr  11148  supsrlem  11149  supsr  11150  ltresr  11178  dfle2  13186  dflt2  13187  dvdszrcl  16292  letsr  18651  hmphtop  23802  brtxp2  35863  brpprod3a  35868  brxrn2  38357  aks6d1c1p1rcl  42090  iccdisj2  48694  i0oii  48716  io1ii  48717