Theorem elisset 2821

Description: An element of a class exists. Use elissetv 2820 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 2820	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴)
2		vextru 2723	. . . . . 6 ⊢ 𝑦 ∈ {𝑧 ∣ ⊤}
3	2	biantru 530	. . . . 5 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
4	3	exbii 1851	. . . 4 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
5		dfclel 2818	. . . 4 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
6	4, 5	bitr4i 277	. . 3 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ 𝐴 ∈ {𝑧 ∣ ⊤})
7		vextru 2723	. . . . . 6 ⊢ 𝑥 ∈ {𝑧 ∣ ⊤}
8	7	biantru 530	. . . . 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 396   = wceq 1539  ⊤wtru 1540  ∃wex 1782   ∈ wcel 2107  {cab 2716

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 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-clel 2817

This theorem is referenced by:  clelab  2884  elex2OLD  3454  elex22  3455  ceqsalt  3463  ceqsalgALT  3466  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  cgsex4gOLD  3478  vtoclgft  3493  vtocld  3495  vtoclg1f  3505  vtoclg  3506  vtocleg  3522  vtoclegft  3523  spcimdv  3533  spcegv  3537  spc2egv  3539  spc2ed  3541  eqvincg  3579  clel2g  3589  clel4g  3594  elabd2  3602  elabgt  3604  elabg  3608  ralsng  4610  dfiun2g  4961  iinexg  5266  ralxfr2d  5334  copsex2t  5407  copsex2gOLD  5409  dmopab2rex  5829  fliftf  7195  eloprabga  7391  eloprabgaOLD  7392  ovmpt4g  7429  eroveu  8610  mreiincl  17314  metustfbas  23722  brabgaf  30957  bnj852  32910  bnj938  32926  bnj1125  32981  bnj1148  32985  bnj1154  32988  fineqvpow  33074  dmopab3rexdif  33376  bj-isseti  35072  bj-ceqsalt  35080  bj-ceqsalg  35083  bj-spcimdv  35089  bj-csbsnlem  35097  bj-vtoclg1f  35112  bj-snsetex  35162  bj-snglc  35168  bj-clel3gALT  35230  copsex2d  35319  prjspeclsp  40458  elex2VD  42465  elex22VD  42466  tpid3gVD  42469  elsprel  44938