Theorem elisset 2847

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-clel 2840

This theorem is used by:  ceqsalt  3490  ceqsalgALT  3493  cgsexg  3501  cgsex2g  3502  cgsex4g  3503  vtocleg  3523  vtocld  3529  vtoclg1f  3537  spcimdv  3554  spcegv  3558  spc2egv  3560  spc2ed  3562  eqvincg  3609  clel2g  3620  clel4g  3624  elabd2  3631  elabgt  3633  elabgtOLD  3634  ralsng  4643  dfiun2g  4996  nvel  5284  iinexg  5320  ralxfr2d  5383  copsex2t  5477  dmopab2rex  5909  fliftf  7322  eloprabga  7528  ovmpt4g  7566  eroveu  8816  mreiincl  17672  metustfbas  24767  brabgaf  33024  bnj852  35376  bnj938  35392  bnj1125  35447  bnj1148  35451  bnj1154  35454  fineqvpow  35587  dmopab3rexdif  35936  rexxfr3dALT  36170  bj-isseti  37572  bj-ceqsalt  37580  bj-ceqsalg  37583  bj-spcimdv  37589  bj-csbsnlem  37597  bj-vtoclg1f  37612  bj-snsetex  37658  bj-snglc  37664  bj-clel3gALT  37743  cgsex2gd  37840  copsex2d  37842  prjspeclsp  43404  elex2VD  45606  elex22VD  45607  tpid3gVD  45610  elsprel  48284