Theorem elisset 2851

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

Syntax hints:   → wi 4   = wceq 1567  ∃wex 1806   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-clel 2844

This theorem is referenced by:  ceqsalt  3496  ceqsalgALT  3499  cgsexg  3507  cgsex2g  3508  cgsex4g  3509  vtocleg  3530  vtocld  3536  vtoclg1f  3544  spcimdv  3561  spcegv  3565  spc2egv  3567  spc2ed  3569  eqvincg  3616  clel2g  3627  clel4g  3631  elabd2  3638  elabgt  3640  elabgtOLD  3641  ralsng  4646  dfiun2g  4998  nvel  5284  iinexg  5319  ralxfr2d  5382  copsex2t  5476  dmopab2rex  5908  fliftf  7314  eloprabga  7520  ovmpt4g  7558  eroveu  8809  mreiincl  17647  metustfbas  24682  brabgaf  32891  bnj852  35253  bnj938  35269  bnj1125  35324  bnj1148  35328  bnj1154  35331  fineqvpow  35450  dmopab3rexdif  35795  rexxfr3dALT  36029  bj-isseti  37401  bj-ceqsalt  37409  bj-ceqsalg  37412  bj-spcimdv  37418  bj-csbsnlem  37426  bj-vtoclg1f  37441  bj-snsetex  37486  bj-snglc  37492  bj-clel3gALT  37571  cgsex2gd  37668  copsex2d  37670  prjspeclsp  43235  elex2VD  45437  elex22VD  45438  tpid3gVD  45441  elsprel  48112