Theorem s2cli 14922

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

Assertion

Ref	Expression
s2cli	⊢ ⟨“𝐴𝐵”⟩ ∈ Word V

Proof of Theorem s2cli

Step	Hyp	Ref	Expression
1		df-s2 14890	. 2 ⊢ ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
2		s1cli 14646	. 2 ⊢ ⟨“𝐴”⟩ ∈ Word V
3	1, 2	cats1cli 14899	1 ⊢ ⟨“𝐴𝐵”⟩ ∈ Word V

Syntax hints:   ∈ wcel 2107  Vcvv 3479  Word cword 14555  ⟨“cs1 14636  ⟨“cs2 14883

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-int 4953  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-1o 8511  df-er 8750  df-en 8991  df-dom 8992  df-sdom 8993  df-fin 8994  df-card 9983  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-hash 14373  df-word 14556  df-concat 14612  df-s1 14637  df-s2 14890

This theorem is referenced by:  s3cli  14923  s2dm  14932  s3fv0  14933  s3fv1  14934  s3fv2  14935  s3len  14936  lsws2  14946  s1s3  14966  s2s2  14971  s4s3  14973  s3s4  14975  pfx2  14989  ccat2s1fvwALT  14997  s3rn  15006  2wlkd  29979  2wlkond  29980  2trlond  29982  2pthond  29985  umgr2adedgwlkonALT  29990  umgr2wlk  29992  1pthon2v  30195  konigsberglem1  30294  konigsberglem2  30295  konigsberglem3  30296  lmat22e12  33793  lmat22e21  33794  lmat22e22  33795  loop1cycl  35134  umgr2cycl  35138