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.

Step	Hyp	Ref	Expression
1		elissetv 2806	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴)
2		vextru 2709	. . . 4 ⊢ 𝑦 ∈ {𝑧 ∣ ⊤}
3	2	issetlem 2805	. . 3 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑦 𝑦 = 𝐴)
4		vextru 2709	. . . 4 ⊢ 𝑥 ∈ {𝑧 ∣ ⊤}
5	4	issetlem 2805	. . 3 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑥 𝑥 = 𝐴)
6	3, 5	bitr3i 276	. 2 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
7	1, 6	sylib 217	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

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