Theorem breldmg 5897

Description: Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
breldmg	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

Proof of Theorem breldmg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5111	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵))
2	1	spcegv 3554	. . . 4 ⊢ (𝐵 ∈ 𝐷 → (𝐴𝑅𝐵 → ∃𝑥 𝐴𝑅𝑥))
3	2	imp 412	. . 3 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → ∃𝑥 𝐴𝑅𝑥)
4		eldmg 5886	. . 3 ⊢ (𝐴 ∈ 𝐶 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝐴𝑅𝑥))
5	3, 4	imbitrrid 249	. 2 ⊢ (𝐴 ∈ 𝐶 → ((𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅))
6	5	3impib 1134	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ dom 𝑅)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103  ∃wex 1812   ∈ wcel 2145   class class class wbr 5107  dom cdm 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-dm 5669

This theorem is used by:  breldmd  5900  brelrng  5929  releldm  5932  sossfld  6183  brtpos  8236  fprresex  8312  tfrlem9a  8378  perpln1  29062  lmdvg  34450  esumcvgsum  34585  climeldmeq  46480  climfv  46506  climxlim2  46661  sge0isum  47242  smflimsuplem6  47640  eubrdm  47911  funressneu  47922  tz6.12-afv  48048  rlimdmafv  48052  tz6.12-afv2  48115  rlimdmafv2  48133