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

Theorem elisset 2807
Description: An element of a class exists. Use elissetv 2806 instead when sufficient (for instance in usages where 𝑥 is a dummy variable). (Contributed by NM, 1-May-1995.) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019.)
Assertion
Ref Expression
elisset (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem elisset
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elissetv 2806 . 2 (𝐴𝑉 → ∃𝑦 𝑦 = 𝐴)
2 vextru 2709 . . . 4 𝑦 ∈ {𝑧 ∣ ⊤}
32issetlem 2805 . . 3 (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑦 𝑦 = 𝐴)
4 vextru 2709 . . . 4 𝑥 ∈ {𝑧 ∣ ⊤}
54issetlem 2805 . . 3 (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑥 𝑥 = 𝐴)
63, 5bitr3i 276 . 2 (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
71, 6sylib 217 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wtru 1534  wex 1773  wcel 2098  {cab 2702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-clel 2802
This theorem is referenced by:  elex2OLD  3485  ceqsalt  3495  ceqsalgALT  3498  cgsexg  3508  cgsex2g  3509  cgsex4g  3510  cgsex4gOLD  3511  cgsex4gOLDOLD  3512  vtocleg  3532  vtocld  3540  vtoclg1f  3550  vtoclgOLD  3551  vtoclegftOLD  3570  spcimdv  3578  spcegv  3582  spc2egv  3584  spc2ed  3586  eqvincg  3632  clel2g  3643  clel4g  3648  elabd2  3656  elabgt  3658  elabgtOLD  3659  elabg  3663  ralsng  4681  dfiun2g  5037  iinexg  5347  ralxfr2d  5413  copsex2t  5497  copsex2gOLD  5499  dmopab2rex  5923  fliftf  7326  eloprabga  7532  eloprabgaOLD  7533  ovmpt4g  7572  eroveu  8840  mreiincl  17604  metustfbas  24549  brabgaf  32519  bnj852  34722  bnj938  34738  bnj1125  34793  bnj1148  34797  bnj1154  34800  fineqvpow  34886  dmopab3rexdif  35185  rexxfr3dALT  35419  bj-isseti  36532  bj-ceqsalt  36540  bj-ceqsalg  36543  bj-spcimdv  36549  bj-csbsnlem  36557  bj-vtoclg1f  36572  bj-snsetex  36618  bj-snglc  36624  bj-clel3gALT  36703  copsex2d  36794  prjspeclsp  42203  elex2VD  44451  elex22VD  44452  tpid3gVD  44455  elsprel  46984
  Copyright terms: Public domain W3C validator