Theorem elisset 2842

Description: An element of a class exists. Use elissetv 2841 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 2841	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴)
2		iseqsetv-clel 2839	. 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	sylib 221	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ∃wex 1811   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-clel 2835

This theorem is used by:  ceqsalt  3483  ceqsalgALT  3486  cgsexg  3494  cgsex2g  3495  cgsex4g  3496  vtocleg  3516  vtocld  3522  vtoclg1f  3530  spcimdv  3547  spcegv  3551  spc2egv  3553  spc2ed  3555  eqvincg  3601  clel2g  3612  clel4g  3616  elabd2  3623  elabgt  3625  elabgtOLD  3626  ralsng  4632  dfiun2g  4987  nvel  5272  iinexg  5309  ralxfr2d  5372  copsex2t  5464  dmopab2rex  5900  fliftf  7327  eloprabga  7533  ovmpt4g  7571  eroveu  8841  mreiincl  17775  metustfbas  24885  brabgaf  33251  bnj852  35601  bnj938  35617  bnj1125  35672  bnj1148  35676  bnj1154  35679  fineqvpow  35851  dmopab3rexdif  36288  rexxfr3dALT  36522  bj-isseti  37914  bj-ceqsalt  37922  bj-ceqsalg  37925  bj-spcimdv  37931  bj-csbsnlem  37939  bj-vtoclg1f  37954  bj-snsetex  38000  bj-snglc  38006  bj-clel3gALT  38099  cgsex2gd  38195  copsex2d  38197  prjspeclsp  43777  elex2VD  45956  elex22VD  45957  tpid3gVD  45960  elsprel  48693