Theorem elisset 2820

Description: An element of a class exists. Use elissetv 2819 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 2819	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴)
2		vextru 2722	. . . . . 6 ⊢ 𝑦 ∈ {𝑧 ∣ ⊤}
3	2	biantru 529	. . . . 5 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
4	3	exbii 1851	. . . 4 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
5		dfclel 2818	. . . 4 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
6	4, 5	bitr4i 277	. . 3 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ 𝐴 ∈ {𝑧 ∣ ⊤})
7		vextru 2722	. . . . . 6 ⊢ 𝑥 ∈ {𝑧 ∣ ⊤}
8	7	biantru 529	. . . . 5 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ ⊤}))
9	8	exbii 1851	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ ⊤}))
10		dfclel 2818	. . . 4 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ ⊤}))
11	9, 10	bitr4i 277	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑧 ∣ ⊤})
12	6, 11	bitr4i 277	. 2 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
13	1, 12	sylib 217	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ⊤wtru 1540  ∃wex 1783   ∈ wcel 2108  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-clel 2817

This theorem is referenced by:  clelab  2882  elex2  3443  elex22  3444  ceqsalt  3452  ceqsalgALT  3455  cgsexg  3464  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  vtoclgft  3482  vtocld  3484  vtoclg1f  3494  vtoclg  3495  vtocleg  3511  vtoclegft  3512  spcimdv  3522  spcegv  3526  spc2egv  3528  spc2ed  3530  eqvincg  3570  clel2g  3581  clel4g  3586  elabd2  3594  elabgt  3596  elabg  3600  ralsng  4606  iinexg  5260  ralxfr2d  5328  copsex2t  5400  copsex2gOLD  5402  dmopab2rex  5815  fliftf  7166  eloprabga  7360  eloprabgaOLD  7361  ovmpt4g  7398  eroveu  8559  mreiincl  17222  metustfbas  23619  brabgaf  30849  bnj852  32801  bnj938  32817  bnj1125  32872  bnj1148  32876  bnj1154  32879  fineqvpow  32965  dmopab3rexdif  33267  bj-isseti  34990  bj-ceqsalt  34998  bj-ceqsalg  35001  bj-spcimdv  35007  bj-csbsnlem  35015  bj-vtoclg1f  35030  bj-snsetex  35080  bj-snglc  35086  bj-clel3gALT  35148  copsex2d  35237  prjspeclsp  40372  elex2VD  42347  elex22VD  42348  tpid3gVD  42351  elsprel  44815