Theorem s1cli 14646

Description: A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
s1cli	⊢ ⟨“𝐴”⟩ ∈ Word V

Proof of Theorem s1cli

Step	Hyp	Ref	Expression
1		ids1 14638	. 2 ⊢ ⟨“𝐴”⟩ = ⟨“( I ‘𝐴)”⟩
2		fvex 6924	. . 3 ⊢ ( I ‘𝐴) ∈ V
3		s1cl 14643	. . 3 ⊢ (( I ‘𝐴) ∈ V → ⟨“( I ‘𝐴)”⟩ ∈ Word V)
4	2, 3	ax-mp 5	. 2 ⊢ ⟨“( I ‘𝐴)”⟩ ∈ Word V
5	1, 4	eqeltri 2836	1 ⊢ ⟨“𝐴”⟩ ∈ Word V

Syntax hints:   ∈ wcel 2107  Vcvv 3479   I cid 5583  ‘cfv 6566  Word cword 14555  ⟨“cs1 14636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5286  ax-sep 5303  ax-nul 5313  ax-pow 5372  ax-pr 5439  ax-un 7758  ax-cnex 11215  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3435  df-v 3481  df-sbc 3793  df-csb 3910  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-pss 3984  df-nul 4341  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4914  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5642  df-we 5644  df-xp 5696  df-rel 5697  df-cnv 5698  df-co 5699  df-dm 5700  df-rn 5701  df-res 5702  df-ima 5703  df-pred 6326  df-ord 6392  df-on 6393  df-lim 6394  df-suc 6395  df-iota 6519  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7392  df-ov 7438  df-oprab 7439  df-mpo 7440  df-om 7892  df-1st 8019  df-2nd 8020  df-frecs 8311  df-wrecs 8342  df-recs 8416  df-rdg 8455  df-er 8750  df-en 8991  df-dom 8992  df-sdom 8993  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11498  df-neg 11499  df-nn 12271  df-n0 12531  df-z 12618  df-uz 12883  df-fz 13551  df-fzo 13698  df-word 14556  df-s1 14637

This theorem is referenced by:  s1dm  14649  eqs1  14653  ccatws1clv  14658  ccats1alpha  14660  ccatws1len  14661  ccat2s1len  14664  ccats1val1  14667  ccat1st1st  14669  ccat2s1p1  14670  ccat2s1p2  14671  ccatw2s1ass  14672  ccat2s1fvw  14679  revs1  14806  cats1cli  14899  cats1fvn  14900  cats1fv  14901  cats1len  14902  cats1cat  14903  cats2cat  14904  s2cli  14922  s2fv0  14929  s2fv1  14930  s2len  14931  s0s1  14964  s1s2  14965  s1s3  14966  s1s4  14967  s1s5  14968  s1s6  14969  s1s7  14970  s2s2  14971  s4s2  14972  s2s5  14976  s5s2  14977  s2rn  15005  s3rn  15006  s7rn  15007  clwwlkwwlksb  30096  clwwlknon1sn  30142  clwwlknon1le1  30143  1pthon2v  30195  wlk2v2e  30199  konigsberglem1  30294  konigsberglem2  30295  konigsberglem3  30296  ccatws1f1o  32934  loop1cycl  35134  mrsubcv  35507  mrsubrn  35510  mvhf1  35556  msubvrs  35557