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

Theorem eldmg 5022
Description: Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
Assertion
Ref Expression
eldmg  |-  ( A  e.  V  ->  ( A  e.  dom  B  <->  E. y  A B y ) )
Distinct variable groups:    y, A    y, B
Allowed substitution hint:    V( y)

Proof of Theorem eldmg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 breq1 4283 . . 3  |-  ( x  =  A  ->  (
x B y  <->  A B
y ) )
21exbidv 1679 . 2  |-  ( x  =  A  ->  ( E. y  x B
y  <->  E. y  A B y ) )
3 df-dm 4837 . 2  |-  dom  B  =  { x  |  E. y  x B y }
42, 3elab2g 3097 1  |-  ( A  e.  V  ->  ( A  e.  dom  B  <->  E. y  A B y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   E.wex 1589    e. wcel 1755   class class class wbr 4280   dom cdm 4827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-dm 4837
This theorem is referenced by:  eldm2g  5023  eldm  5024  breldmg  5032  releldmb  5061  funeu  5430  fneu  5503  ndmfv  5702  suppvalbr  6683  erref  7109  ecdmn0  7131  rlimdm  13013  rlimdmo1  13079  iscmet3lem2  20645  dvcnp2  21236  ulmcau  21745  pserulm  21772  mulog2sum  22671  afveu  29905  rlimdmafv  29929
  Copyright terms: Public domain W3C validator