Theorem eldmg 5863

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1550  ∃wex 1789   ∈ wcel 2132   class class class wbr 5090  dom cdm 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-dm 5646

This theorem is referenced by:  eldm2g  5864  eldm  5865  breldmg  5874  releldmb  5911  funeu  6531  fneu  6616  ndmfv  6884  erref  8683  ecdmn0  8715  rlimdm  15550  rlimdmo1  15617  iscmet3lem2  25323  dvcnp2  25951  ulmcau  26424  pserulm  26451  mulog2sum  27567  unbdqndv1  36884  eldmres  38714  eldmressnALTV  38716  eldm4  38718  eldmres2  38719  eldmcnv  38782  ssdmral  38816  eldisjdmqsim  39254  funressneu  47579  afveu  47685  rlimdmafv  47709  funressndmafv2rn  47755  afv2eu  47770  rlimdmafv2  47790  uobrcl  49752  uobeq2  49960