Theorem eldmg 5848

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114   class class class wbr 5099  dom cdm 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-dm 5635

This theorem is referenced by:  eldm2g  5849  eldm  5850  breldmg  5859  releldmb  5896  funeu  6518  fneu  6603  ndmfv  6867  erref  8659  ecdmn0  8691  rlimdm  15479  rlimdmo1  15546  iscmet3lem2  25253  dvcnp2  25882  dvcnp2OLD  25883  ulmcau  26365  pserulm  26392  mulog2sum  27509  unbdqndv1  36721  eldmres  38491  eldmressnALTV  38493  eldm4  38495  eldmres2  38496  eldmcnv  38559  ssdmral  38593  eldisjdmqsim  39031  funressneu  47370  afveu  47476  rlimdmafv  47500  funressndmafv2rn  47546  afv2eu  47561  rlimdmafv2  47581  uobrcl  49515  uobeq2  49723