MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldmg Structured version   Visualization version   GIF version

Theorem eldmg 5767
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.
StepHypRef Expression
1 breq1 5056 . . 3 (𝑥 = 𝐴 → (𝑥𝐵𝑦𝐴𝐵𝑦))
21exbidv 1929 . 2 (𝑥 = 𝐴 → (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦 𝐴𝐵𝑦))
3 df-dm 5561 . 2 dom 𝐵 = {𝑥 ∣ ∃𝑦 𝑥𝐵𝑦}
42, 3elab2g 3589 1 (𝐴𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1543  wex 1787  wcel 2110   class class class wbr 5053  dom cdm 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-dm 5561
This theorem is referenced by:  eldm2g  5768  eldm  5769  breldmg  5778  releldmb  5815  funeu  6405  fneu  6488  ndmfv  6747  erref  8411  ecdmn0  8438  rlimdm  15112  rlimdmo1  15179  iscmet3lem2  24189  dvcnp2  24817  ulmcau  25287  pserulm  25314  mulog2sum  26418  unbdqndv1  34425  eldmres  36145  eldm4  36146  eldmres2  36147  eldmcnv  36217  funressneu  44213  afveu  44317  rlimdmafv  44341  funressndmafv2rn  44387  afv2eu  44402  rlimdmafv2  44422
  Copyright terms: Public domain W3C validator