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

Theorem eldmg 5457
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 4787 . . 3 (𝑥 = 𝐴 → (𝑥𝐵𝑦𝐴𝐵𝑦))
21exbidv 2001 . 2 (𝑥 = 𝐴 → (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦 𝐴𝐵𝑦))
3 df-dm 5259 . 2 dom 𝐵 = {𝑥 ∣ ∃𝑦 𝑥𝐵𝑦}
42, 3elab2g 3502 1 (𝐴𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1630  wex 1851  wcel 2144   class class class wbr 4784  dom cdm 5249
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785  df-dm 5259
This theorem is referenced by:  eldm2g  5458  eldm  5459  breldmg  5468  releldmb  5498  funeu  6056  fneu  6135  ndmfv  6359  erref  7915  ecdmn0  7940  rlimdm  14489  rlimdmo1  14555  iscmet3lem2  23308  dvcnp2  23902  ulmcau  24368  pserulm  24395  mulog2sum  25446  unbdqndv1  32830  eldmres  34372  eldm4  34373  eldmres2  34374  eldmcnv  34448  afveu  41747  rlimdmafv  41771
  Copyright terms: Public domain W3C validator