Theorem elisset 3506

Description: An element of a class exists. (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		exsimpl 1865	. 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → ∃𝑦 𝑦 = 𝐴)
2		dfclel 2894	. 2 ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉))
3		eqeq1 2825	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴))
4	3	cbvexvw 2040	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
5	1, 2, 4	3imtr4i 294	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533  ∃wex 1776   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893

This theorem is referenced by:  isseti  3509  elex2  3517  elex22  3518  ceqsalt  3528  ceqsalgALT  3531  cgsexg  3538  cgsex2g  3539  cgsex4g  3540  vtoclgft  3554  vtoclgftOLD  3555  vtoclg1f  3567  vtocleg  3581  vtoclegft  3582  spcimdv  3592  spcegv  3597  spc2egv  3600  spc2ed  3602  eqvincg  3641  iinexg  5237  ralxfr2d  5303  copsex2t  5376  copsex2g  5377  dmopab2rex  5781  fliftf  7062  eloprabga  7255  ovmpt4g  7291  eroveu  8386  mreiincl  16861  metustfbas  23161  brabgaf  30353  bnj852  32188  bnj938  32204  bnj1125  32259  bnj1148  32263  bnj1154  32266  dmopab3rexdif  32647  bj-csbsnlem  34215  bj-snsetex  34270  bj-snglc  34276  copsex2d  34425  prjspeclsp  39255  elex2VD  41165  elex22VD  41166  tpid3gVD  41169  elsprel  43630