Theorem elisset 2812

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 variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elissetv 2811	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴)
2		vextru 2721	. . . . . 6 ⊢ 𝑦 ∈ {𝑧 ∣ ⊤}
3	2	biantru 533	. . . . 5 ⊢ (𝑦 = 𝐴 ↔ (𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
4	3	exbii 1855	. . . 4 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
5		dfclel 2810	. . . 4 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑧 ∣ ⊤}))
6	4, 5	bitr4i 281	. . 3 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ 𝐴 ∈ {𝑧 ∣ ⊤})
7		vextru 2721	. . . . . 6 ⊢ 𝑥 ∈ {𝑧 ∣ ⊤}
8	7	biantru 533	. . . . 5 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ ⊤}))
9	8	exbii 1855	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ ⊤}))
10		dfclel 2810	. . . 4 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ {𝑧 ∣ ⊤}))
11	9, 10	bitr4i 281	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑧 ∣ ⊤})
12	6, 11	bitr4i 281	. 2 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴)
13	1, 12	sylib 221	1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543  ⊤wtru 1544  ∃wex 1787   ∈ wcel 2112  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-clel 2809

This theorem is referenced by:  clelab  2873  elex2  3419  elex22  3420  ceqsalt  3428  ceqsalgALT  3431  cgsexg  3440  cgsex2g  3441  cgsex4g  3442  cgsex4gOLD  3443  vtoclgft  3458  vtocld  3460  vtoclg1f  3470  vtoclg  3471  vtocleg  3487  vtoclegft  3488  spcimdv  3498  spcegv  3502  spc2egv  3504  spc2ed  3506  eqvincg  3545  clel2g  3556  clel4g  3561  elabd2  3569  elabgt  3570  elabg  3574  ralsng  4575  iinexg  5219  ralxfr2d  5288  copsex2t  5360  copsex2gOLD  5362  dmopab2rex  5771  fliftf  7102  eloprabga  7296  eloprabgaOLD  7297  ovmpt4g  7334  eroveu  8472  mreiincl  17053  metustfbas  23409  brabgaf  30621  bnj852  32568  bnj938  32584  bnj1125  32639  bnj1148  32643  bnj1154  32646  fineqvpow  32732  dmopab3rexdif  33034  bj-csbsnlem  34775  bj-snsetex  34839  bj-snglc  34845  bj-clel3gALT  34907  copsex2d  34994  prjspeclsp  40100  elex2VD  42072  elex22VD  42073  tpid3gVD  42076  elsprel  44543