Theorem elisset 2816

Description: An element of a class exists. Use elissetv 2815 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 2815	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴)
2		vextru 2717	. . . 4 ⊢ 𝑦 ∈ {𝑧 ∣ ⊤}
3	2	issetlem 2814	. . 3 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑦 𝑦 = 𝐴)
4		vextru 2717	. . . 4 ⊢ 𝑥 ∈ {𝑧 ∣ ⊤}
5	4	issetlem 2814	. . 3 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑥 𝑥 = 𝐴)
6	3, 5	bitr3i 277	. 2 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
7	1, 6	sylib 217	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  ⊤wtru 1543  ∃wex 1782   ∈ wcel 2107  {cab 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-clel 2811

This theorem is referenced by:  elex2OLD  3496  ceqsalt  3506  ceqsalgALT  3509  cgsexg  3519  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  vtocld  3543  vtocleg  3546  vtoclg1f  3556  vtoclgOLD  3558  vtoclegftOLD  3575  spcimdv  3584  spcegv  3588  spc2egv  3590  spc2ed  3592  eqvincg  3637  clel2g  3648  clel4g  3653  elabd2  3661  elabgt  3663  elabg  3667  ralsng  4678  dfiun2g  5034  iinexg  5342  ralxfr2d  5409  copsex2t  5493  copsex2gOLD  5495  dmopab2rex  5918  fliftf  7312  eloprabga  7516  eloprabgaOLD  7517  ovmpt4g  7555  eroveu  8806  mreiincl  17540  metustfbas  24066  brabgaf  31868  bnj852  33963  bnj938  33979  bnj1125  34034  bnj1148  34038  bnj1154  34041  fineqvpow  34127  dmopab3rexdif  34427  bj-isseti  35806  bj-ceqsalt  35814  bj-ceqsalg  35817  bj-spcimdv  35823  bj-csbsnlem  35831  bj-vtoclg1f  35846  bj-snsetex  35892  bj-snglc  35898  bj-clel3gALT  35977  copsex2d  36068  prjspeclsp  41402  elex2VD  43647  elex22VD  43648  tpid3gVD  43651  elsprel  46191