Theorem eldmg 5888

Description: Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)

Assertion

Ref	Expression
eldmg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵

Allowed substitution hint:   𝑉(𝑦)

Proof of Theorem eldmg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5111	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥𝐵𝑦 ↔ 𝐴𝐵𝑦))
2	1	exbidv 1949	. 2 ⊢ (𝑥 = 𝐴 → (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦 𝐴𝐵𝑦))
3		df-dm 5671	. 2 ⊢ dom 𝐵 = {𝑥 ∣ ∃𝑦 𝑥𝐵𝑦}
4	2, 3	elab2g 3638	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568  ∃wex 1807   ∈ wcel 2141   class class class wbr 5108  dom cdm 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-dm 5671

This theorem is referenced by:  eldm2g  5889  eldm  5890  breldmg  5899  releldmb  5936  funeu  6561  fneu  6645  ndmfv  6913  erref  8714  ecdmn0  8746  rlimdm  15601  rlimdmo1  15668  iscmet3lem2  25430  dvcnp2  26058  ulmcau  26534  pserulm  26561  mulog2sum  27677  unbdqndv1  37041  eldmres  38872  eldmressnALTV  38874  eldm4  38876  eldmres2  38877  eldmcnv  38940  ssdmral  38974  eldisjdmqsim  39412  funressneu  47729  afveu  47835  rlimdmafv  47859  funressndmafv2rn  47905  afv2eu  47920  rlimdmafv2  47940  uobrcl  49916  uobeq2  50124