Theorem s1cli 13939

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 13931	. 2 ⊢ ⟨“𝐴”⟩ = ⟨“( I ‘𝐴)”⟩
2		fvex 6664	. . 3 ⊢ ( I ‘𝐴) ∈ V
3		s1cl 13936	. . 3 ⊢ (( I ‘𝐴) ∈ V → ⟨“( I ‘𝐴)”⟩ ∈ Word V)
4	2, 3	ax-mp 5	. 2 ⊢ ⟨“( I ‘𝐴)”⟩ ∈ Word V
5	1, 4	eqeltri 2907	1 ⊢ ⟨“𝐴”⟩ ∈ Word V

Syntax hints:   ∈ wcel 2114  Vcvv 3481   I cid 5440  ‘cfv 6336  Word cword 13846  ⟨“cs1 13929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7442  ax-cnex 10574  ax-resscn 10575  ax-1cn 10576  ax-icn 10577  ax-addcl 10578  ax-addrcl 10579  ax-mulcl 10580  ax-mulrcl 10581  ax-mulcom 10582  ax-addass 10583  ax-mulass 10584  ax-distr 10585  ax-i2m1 10586  ax-1ne0 10587  ax-1rid 10588  ax-rnegex 10589  ax-rrecex 10590  ax-cnre 10591  ax-pre-lttri 10592  ax-pre-lttrn 10593  ax-pre-ltadd 10594  ax-pre-mulgt0 10595

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3012  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3483  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7095  df-ov 7140  df-oprab 7141  df-mpo 7142  df-om 7562  df-1st 7670  df-2nd 7671  df-wrecs 7928  df-recs 7989  df-rdg 8027  df-er 8270  df-en 8491  df-dom 8492  df-sdom 8493  df-pnf 10658  df-mnf 10659  df-xr 10660  df-ltxr 10661  df-le 10662  df-sub 10853  df-neg 10854  df-nn 11620  df-n0 11880  df-z 11964  df-uz 12226  df-fz 12878  df-fzo 13019  df-word 13847  df-s1 13930

This theorem is referenced by:  s1dm  13942  eqs1  13946  ccatws1clv  13951  ccats1alpha  13953  ccatws1len  13954  ccat2s1len  13957  ccats1val1  13961  ccat1st1st  13964  ccat2s1p1  13965  ccat2s1p2  13966  ccatw2s1ass  13969  ccat2s1fvw  13978  revs1  14107  cats1cli  14199  cats1fvn  14200  cats1fv  14201  cats1len  14202  cats1cat  14203  cats2cat  14204  s2cli  14222  s2fv0  14229  s2fv1  14230  s2len  14231  s0s1  14264  s1s2  14265  s1s3  14266  s1s4  14267  s1s5  14268  s1s6  14269  s1s7  14270  s2s2  14271  s4s2  14272  s2s5  14276  s5s2  14277  clwwlkwwlksb  27812  clwwlknon1sn  27858  clwwlknon1le1  27859  1pthon2v  27911  wlk2v2e  27915  konigsberglem1  28010  konigsberglem2  28011  konigsberglem3  28012  loop1cycl  32386  mrsubcv  32759  mrsubrn  32762  mvhf1  32808  msubvrs  32809