Theorem eldmg 5852

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 5105	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥𝐵𝑦 ↔ 𝐴𝐵𝑦))
2	1	exbidv 1921	. 2 ⊢ (𝑥 = 𝐴 → (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦 𝐴𝐵𝑦))
3		df-dm 5641	. 2 ⊢ dom 𝐵 = {𝑥 ∣ ∃𝑦 𝑥𝐵𝑦}
4	2, 3	elab2g 3644	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109   class class class wbr 5102  dom cdm 5631

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  eldm2g  5853  eldm  5854  breldmg  5863  releldmb  5899  funeu  6525  fneu  6610  ndmfv  6875  erref  8668  ecdmn0  8700  rlimdm  15494  rlimdmo1  15561  iscmet3lem2  25226  dvcnp2  25855  dvcnp2OLD  25856  ulmcau  26338  pserulm  26365  mulog2sum  27482  unbdqndv1  36490  eldmres  38253  eldmressnALTV  38255  eldm4  38257  eldmres2  38258  eldmcnv  38321  funressneu  47042  afveu  47148  rlimdmafv  47172  funressndmafv2rn  47218  afv2eu  47233  rlimdmafv2  47253  uobrcl  49176  uobeq2  49384