Theorem eldmg 5846

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

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

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-dm 5633

This theorem is referenced by:  eldm2g  5847  eldm  5848  breldmg  5857  releldmb  5894  funeu  6516  fneu  6601  ndmfv  6865  erref  8656  ecdmn0  8688  rlimdm  15476  rlimdmo1  15543  iscmet3lem2  25250  dvcnp2  25879  dvcnp2OLD  25880  ulmcau  26362  pserulm  26389  mulog2sum  27506  unbdqndv1  36681  eldmres  38447  eldmressnALTV  38449  eldm4  38451  eldmres2  38452  eldmcnv  38515  ssdmral  38549  eldisjdmqsim  38987  funressneu  47330  afveu  47436  rlimdmafv  47460  funressndmafv2rn  47506  afv2eu  47521  rlimdmafv2  47541  uobrcl  49475  uobeq2  49683