Theorem elisset 2823

Description: An element of a class exists. Use elissetv 2822 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 variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elissetv 2822	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴)
2		iseqsetv-clel 2820	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	sylib 218	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-clel 2816

This theorem is referenced by:  elex2OLD  3505  ceqsalt  3515  ceqsalgALT  3518  cgsexg  3526  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  vtocleg  3553  vtocld  3561  vtoclg1f  3570  vtoclgOLD  3571  vtoclegftOLD  3589  spcimdv  3593  spcegv  3597  spc2egv  3599  spc2ed  3601  eqvincg  3648  clel2g  3659  clel4g  3663  elabd2  3670  elabgt  3672  elabgtOLD  3673  elabg  3676  ralsng  4675  dfiun2g  5030  iinexg  5348  ralxfr2d  5410  copsex2t  5497  dmopab2rex  5928  fliftf  7335  eloprabga  7542  ovmpt4g  7580  eroveu  8852  mreiincl  17639  metustfbas  24570  brabgaf  32620  bnj852  34935  bnj938  34951  bnj1125  35006  bnj1148  35010  bnj1154  35013  fineqvpow  35110  dmopab3rexdif  35410  rexxfr3dALT  35644  bj-isseti  36879  bj-ceqsalt  36887  bj-ceqsalg  36890  bj-spcimdv  36896  bj-csbsnlem  36904  bj-vtoclg1f  36919  bj-snsetex  36964  bj-snglc  36970  bj-clel3gALT  37049  copsex2d  37140  prjspeclsp  42622  elex2VD  44858  elex22VD  44859  tpid3gVD  44862  elsprel  47462