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

Theorem eldmg 5732
 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 5034 . . 3 (𝑥 = 𝐴 → (𝑥𝐵𝑦𝐴𝐵𝑦))
21exbidv 1922 . 2 (𝑥 = 𝐴 → (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦 𝐴𝐵𝑦))
3 df-dm 5530 . 2 dom 𝐵 = {𝑥 ∣ ∃𝑦 𝑥𝐵𝑦}
42, 3elab2g 3616 1 (𝐴𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2111   class class class wbr 5031  dom cdm 5520 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5032  df-dm 5530 This theorem is referenced by:  eldm2g  5733  eldm  5734  breldmg  5743  releldmb  5781  funeu  6350  fneu  6433  ndmfv  6676  erref  8295  ecdmn0  8322  rlimdm  14903  rlimdmo1  14969  iscmet3lem2  23906  dvcnp2  24533  ulmcau  25000  pserulm  25027  mulog2sum  26131  unbdqndv1  33975  eldmres  35709  eldm4  35710  eldmres2  35711  eldmcnv  35781  funressneu  43682  afveu  43752  rlimdmafv  43776  funressndmafv2rn  43822  afv2eu  43837  rlimdmafv2  43857
 Copyright terms: Public domain W3C validator