Theorem 1cex 4142

Description: Cardinal one is a set. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
1cex	⊢ 1c ∈ V

Proof of Theorem 1cex

Dummy variables x y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1c 4081	. 2 ⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z))
2		isset 2863	. . 3 ⊢ (1c ∈ V ↔ ∃x x = 1c)
3		df-1c 4136	. . . . . . 7 ⊢ 1c = {y ∣ ∃z y = {z}}
4	3	eqeq2i 2363	. . . . . 6 ⊢ (x = 1c ↔ x = {y ∣ ∃z y = {z}})
5		abeq2 2458	. . . . . 6 ⊢ (x = {y ∣ ∃z y = {z}} ↔ ∀y(y ∈ x ↔ ∃z y = {z}))
6	4, 5	bitri 240	. . . . 5 ⊢ (x = 1c ↔ ∀y(y ∈ x ↔ ∃z y = {z}))
7		dfcleq 2347	. . . . . . . . 9 ⊢ (y = {z} ↔ ∀w(w ∈ y ↔ w ∈ {z}))
8		df-sn 3741	. . . . . . . . . . . 12 ⊢ {z} = {w ∣ w = z}
9	8	abeq2i 2460	. . . . . . . . . . 11 ⊢ (w ∈ {z} ↔ w = z)
10	9	bibi2i 304	. . . . . . . . . 10 ⊢ ((w ∈ y ↔ w ∈ {z}) ↔ (w ∈ y ↔ w = z))
11	10	albii 1566	. . . . . . . . 9 ⊢ (∀w(w ∈ y ↔ w ∈ {z}) ↔ ∀w(w ∈ y ↔ w = z))
12	7, 11	bitri 240	. . . . . . . 8 ⊢ (y = {z} ↔ ∀w(w ∈ y ↔ w = z))
13	12	exbii 1582	. . . . . . 7 ⊢ (∃z y = {z} ↔ ∃z∀w(w ∈ y ↔ w = z))
14	13	bibi2i 304	. . . . . 6 ⊢ ((y ∈ x ↔ ∃z y = {z}) ↔ (y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)))
15	14	albii 1566	. . . . 5 ⊢ (∀y(y ∈ x ↔ ∃z y = {z}) ↔ ∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)))
16	6, 15	bitri 240	. . . 4 ⊢ (x = 1c ↔ ∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)))
17	16	exbii 1582	. . 3 ⊢ (∃x x = 1c ↔ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)))
18	2, 17	bitri 240	. 2 ⊢ (1c ∈ V ↔ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z)))
19	1, 18	mpbir 200	1 ⊢ 1c ∈ V

Syntax hints:   ↔ wb 176  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  Vcvv 2859  {csn 3737  1_cc1c 4134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-1c 4081

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861  df-sn 3741  df-1c 4136

This theorem is referenced by:  sikexg  4296  imakexg  4299  ins2kexg  4305  ins3kexg  4306  imagekexg  4311  pwexg  4328  addcexlem  4382  nncex  4396  peano2  4403  findsd  4410  nnc0suc  4412  nnsucelrlem1  4424  nndisjeq  4429  ltfinp1  4462  ltfinex  4464  ssfin  4470  ncfinraiselem2  4480  ncfinlowerlem1  4482  tfinrelkex  4487  tfin1c  4499  evenfinex  4503  oddfinex  4504  sucevenodd  4510  sucoddeven  4511  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelkex  4525  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  1cvsfin  4542  vfin1cltv  4547  vfinncvntnn  4548  vfinspsslem1  4550  phiexg  4571  opexg  4587  proj1exg  4591  proj2exg  4592  phi11lem1  4595  phialllem1  4616  setconslem5  4735  1stex  4739  swapex  4742  imageexg  5800  mptexlem  5810  mpt2exlem  5811  composeex  5820  disjex  5823  addcfnex  5824  funsex  5828  crossex  5850  pw1fnex  5852  domfnex  5870  ranfnex  5871  dfnnc3  5885  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  qsexg  5982  enprmaplem1  6076  mucex  6133  ovcelem1  6171  ceex  6174  ce2ncpw11c  6194  nc0le1  6216  tcnc1c  6227  ce0lenc1  6239  tlenc1c  6240  tcfnex  6244  csucex  6259  nnltp1clem1  6261  nmembers1lem1  6268  nncdiv3lem2  6276  nnc3n3p1  6278  nchoicelem8  6296  nchoicelem9  6297  nchoicelem11  6299  nchoicelem16  6304  nchoicelem18  6306  dmfrec  6316  fnfreclem2  6318  fnfreclem3  6319