Theorem eldmg 5887

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1808   ∈ wcel 2142   class class class wbr 5108  dom cdm 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  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 5670

This theorem is used by:  eldm2g  5888  eldm  5889  breldmg  5898  releldmb  5935  funeu  6561  fneu  6645  ndmfv  6913  erref  8713  ecdmn0  8745  rlimdm  15609  rlimdmo1  15676  iscmet3lem2  25462  dvcnp2  26090  ulmcau  26569  pserulm  26596  mulog2sum  27712  unbdqndv1  37125  eldmres  38954  eldmressnALTV  38956  eldm4  38958  eldmres2  38959  eldmcnv  39022  ssdmral  39056  eldisjdmqsim  39494  funressneu  47812  afveu  47918  rlimdmafv  47942  funressndmafv2rn  47988  afv2eu  48003  rlimdmafv2  48023  uobrcl  49999  uobeq2  50207