Theorem elisset 2819

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1541  ⊤wtru 1542  ∃wex 1781   ∈ wcel 2106  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-clel 2815

This theorem is referenced by:  clelab  2881  elex2OLD  3463  elex22  3464  ceqsalt  3472  ceqsalgALT  3475  cgsexg  3484  cgsex2g  3485  cgsex4g  3486  cgsex4gOLD  3487  vtoclgft  3504  vtocld  3506  vtoclg1f  3516  vtoclg  3517  vtocleg  3533  vtoclegft  3534  spcimdv  3544  spcegv  3548  spc2egv  3550  spc2ed  3552  eqvincg  3590  clel2g  3601  clel4g  3606  elabd2  3614  elabgt  3616  elabg  3620  ralsng  4625  dfiun2g  4981  iinexg  5289  ralxfr2d  5357  copsex2t  5440  copsex2gOLD  5442  dmopab2rex  5863  fliftf  7246  eloprabga  7448  eloprabgaOLD  7449  ovmpt4g  7486  eroveu  8676  mreiincl  17402  metustfbas  23818  brabgaf  31233  bnj852  33198  bnj938  33214  bnj1125  33269  bnj1148  33273  bnj1154  33276  fineqvpow  33362  dmopab3rexdif  33664  bj-isseti  35199  bj-ceqsalt  35207  bj-ceqsalg  35210  bj-spcimdv  35216  bj-csbsnlem  35224  bj-vtoclg1f  35239  bj-snsetex  35288  bj-snglc  35294  bj-clel3gALT  35373  copsex2d  35464  prjspeclsp  40762  elex2VD  42831  elex22VD  42832  tpid3gVD  42835  elsprel  45345