Theorem 1cex 4143

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 4082	. 2 ⊢ ∃x∀y(y ∈ x ↔ ∃z∀w(w ∈ y ↔ w = z))
2		isset 2864	. . 3 ⊢ (1c ∈ V ↔ ∃x x = 1c)
3		df-1c 4137	. . . . . . 7 ⊢ 1c = {y ∣ ∃z y = {z}}
4	3	eqeq2i 2363	. . . . . 6 ⊢ (x = 1c ↔ x = {y ∣ ∃z y = {z}})
5		abeq2 2459	. . . . . 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 3742	. . . . . . . . . . . 12 ⊢ {z} = {w ∣ w = z}
9	8	abeq2i 2461	. . . . . . . . . . 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 2860  {csn 3738  1_cc1c 4135

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 4082

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 2862  df-sn 3742  df-1c 4137

This theorem is referenced by:  sikexg  4297  imakexg  4300  ins2kexg  4306  ins3kexg  4307  imagekexg  4312  pwexg  4329  addcexlem  4383  nncex  4397  peano2  4404  findsd  4411  nnc0suc  4413  nnsucelrlem1  4425  nndisjeq  4430  ltfinp1  4463  ltfinex  4465  ssfin  4471  ncfinraiselem2  4481  ncfinlowerlem1  4483  tfinrelkex  4488  tfin1c  4500  evenfinex  4504  oddfinex  4505  sucevenodd  4511  sucoddeven  4512  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelkex  4526  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  1cvsfin  4543  vfin1cltv  4548  vfinncvntnn  4549  vfinspsslem1  4551  phiexg  4572  opexg  4588  proj1exg  4592  proj2exg  4593  phi11lem1  4596  phialllem1  4617  setconslem5  4736  1stex  4740  swapex  4743  imageexg  5801  mptexlem  5811  mpt2exlem  5812  composeex  5821  disjex  5824  addcfnex  5825  funsex  5829  crossex  5851  pw1fnex  5853  domfnex  5871  ranfnex  5872  dfnnc3  5886  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  qsexg  5983  enprmaplem1  6077  mucex  6134  ovcelem1  6172  ceex  6175  ce2ncpw11c  6195  nc0le1  6217  tcnc1c  6228  ce0lenc1  6240  tlenc1c  6241  tcfnex  6245  csucex  6260  nnltp1clem1  6262  nmembers1lem1  6269  nncdiv3lem2  6277  nnc3n3p1  6279  nchoicelem8  6297  nchoicelem9  6298  nchoicelem11  6300  nchoicelem16  6305  nchoicelem18  6307  dmfrec  6317  fnfreclem2  6319  fnfreclem3  6320