MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq2i Structured version   Visualization version   GIF version

Theorem oveq2i 7156
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveq2i (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq2 7153 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148
This theorem is referenced by:  caov32  7364  caov4  7368  caov42  7370  seqomsuc  8084  oa1suc  8147  o2p2e4  8157  om1  8158  oe1  8160  oawordeulem  8170  oeoalem  8212  nnm1  8265  nnm2  8266  nneob  8269  omopthlem1  8272  mapsnconst  8445  mapsncnv  8446  map2xp  8676  cantnflt  9124  cnfcom2  9154  infxpenc  9433  infxpenc2  9437  mapdjuen  9595  ackbij1lem5  9635  alephom  9996  pwxpndom2  10076  adderpqlem  10365  addassnq  10369  mulcanenq  10371  distrnq  10372  ltanq  10382  ltexnq  10386  halfnq  10387  ltrnq  10390  archnq  10391  addclprlem2  10428  prlem934  10444  prlem936  10458  addcmpblnr  10480  mulcmpblnrlem  10481  ltsrpr  10488  m1p1sr  10503  m1m1sr  10504  0idsr  10508  1idsr  10509  00sr  10510  pn0sr  10512  recexsrlem  10514  mulgt0sr  10516  sqgt0sr  10517  mulresr  10550  axmulcom  10566  axmulass  10568  axdistr  10569  axi2m1  10570  ax1rid  10572  axcnre  10575  mul02lem1  10805  addid1  10809  negid  10922  negsub  10923  subneg  10924  negsubdii  10960  muleqadd  11273  crne0  11620  2p2e4  11761  1p2e3  11769  3p2e5  11777  3p3e6  11778  4p2e6  11779  4p3e7  11780  4p4e8  11781  5p2e7  11782  5p3e8  11783  5p4e9  11784  6p2e8  11785  6p3e9  11786  7p2e9  11787  3t3e9  11793  8th4div3  11846  halfpm6th  11847  addltmul  11862  div4p1lem1div2  11881  nn0n0n1ge2  11951  nneo  12055  zeo  12057  numsuc  12101  numltc  12113  numsucc  12127  numma  12131  nummul1c  12136  decrmac  12145  decsubi  12150  decmul10add  12156  6p5lem  12157  5p5e10  12158  6p4e10  12159  7p3e10  12162  8p2e10  12167  4t3lem  12184  9t11e99  12217  decbin2  12228  xmulmnf1  12659  fztp  12953  fz12pr  12954  fztpval  12959  fzshftral  12985  fz0tp  12998  fz0to3un2pr  12999  fzo01  13109  fzo12sn  13110  fzo13pr  13111  fzo0to2pr  13112  fzo0to3tp  13113  fzo0to42pr  13114  fzo1to4tp  13115  fzosplitprm1  13137  quoremz  13213  quoremnn0ALT  13215  intfrac2  13216  intfracq  13217  sqval  13471  sqrecii  13536  sq4e2t8  13552  cu2  13553  i3  13556  i4  13557  binom2i  13564  binom3  13575  crreczi  13579  3dec  13616  nn0opthlem1  13618  facp1  13628  faclbnd  13640  faclbnd2  13641  faclbnd4lem1  13643  faclbnd4lem4  13646  bcn1  13663  bcn2  13669  4bc3eq4  13678  4bc2eq6  13679  hashgadd  13728  hashxplem  13784  hashmap  13786  hashfun  13788  hashbclem  13800  fz1isolem  13809  ccatlid  13930  ccatrid  13931  ccatws1len  13964  ccats1val2  13973  ccat2s1p2  13976  ccat2s1p2OLD  13978  pfx1  14055  pfxccatin12lem3  14084  pfxccatpfx1  14088  pfxccatpfx2  14089  cats1fvn  14210  cats1cat  14213  cats2cat  14214  s3fn  14263  swrds2  14292  swrds2m  14293  reim0  14467  cji  14508  sqrtm1  14625  absi  14636  rddif  14690  iseraltlem2  15029  iseralt  15031  fsump1i  15114  fsummulc2  15129  incexclem  15181  incexc  15182  arisum2  15206  geoihalfsum  15228  mertenslem1  15230  mertens  15232  risefall0lem  15370  risefac1  15377  fallfac1  15378  fallfacfwd  15380  bpoly0  15394  bpoly1  15395  bpolydiflem  15398  bpoly2  15401  bpoly3  15402  bpoly4  15403  fsumcube  15404  ef0lem  15422  ege2le3  15433  eft0val  15455  ef4p  15456  efgt1p2  15457  efgt1p  15458  tanval2  15476  efival  15495  ef01bndlem  15527  sin01bnd  15528  cos01bnd  15529  cos1bnd  15530  cos2bnd  15531  rpnnen2lem11  15567  3dvdsdec  15671  3dvds2dec  15672  odd2np1lem  15679  odd2np1  15680  oddp1even  15683  opoe  15702  divalglem5  15738  divalglem6  15739  bits0  15767  0bits  15778  gcdaddmlem  15862  6gcd4e2  15876  lcmneg  15937  3lcm2e6woprm  15949  6lcm4e12  15950  3prm  16028  3lcm2e6  16062  phiprm  16104  eulerthlem2  16109  prmdiv  16112  pythagtriplem12  16153  pythagtriplem14  16155  pcmpt  16218  pcfac  16225  prmpwdvds  16230  pockthi  16233  prmreclem2  16243  prmreclem6  16247  4sqlem5  16268  4sqlem13  16283  modxai  16394  mod2xnegi  16397  gcdi  16399  decexp2  16401  numexpp1  16404  numexp2x  16405  decsplit0b  16406  decsplit1  16408  decsplit  16409  2exp16  16414  prmlem0  16429  139prm  16447  163prm  16448  317prm  16449  631prm  16450  1259lem4  16457  1259lem5  16458  1259prm  16459  2503lem1  16460  2503lem2  16461  2503lem3  16462  2503prm  16463  4001lem1  16464  4001lem4  16467  ressinbas  16550  rcaninv  17054  rescfth  17197  xpccatid  17428  oduval  17730  oppgmnd  18422  psgnunilem2  18554  psgnunilem4  18556  psgnpmtr  18569  psgn0fv0  18570  psgnsn  18579  psgnprfval1  18581  lsmmod2  18733  efgi0  18777  efgi1  18778  efginvrel2  18784  efgsval2  18790  efgsp1  18794  efgredleme  18800  efgredlemc  18802  efgcpbllemb  18812  frgpnabllem1  18924  lt6abl  18946  gsumconstf  18986  gsum2dlem2  19022  pwsgsum  19033  fsfnn0gsumfsffz  19034  dprd0  19084  dprdf1  19086  dprd2da  19095  ablfac1lem  19121  pgpfac1lem3  19130  pgpfaclem1  19134  srgbinomlem4  19224  opprring  19312  mulgass3  19318  evlsval  20229  mpff  20247  ply1assa  20297  gsumply1subr  20332  ply1coe  20394  coe1fzgsumdlem  20399  coe1fzgsumd  20400  gsumply1eq  20403  evl1gsumdlem  20449  evl1gsumd  20450  xrsnsgrp  20511  znbas  20620  znzrh2  20622  dsmmval2  20810  frlmip  20852  matgsum  20976  madetsumid  21000  mdetrsca  21142  mdetrsca2  21143  mdettpos  21150  m2detleiblem2  21167  madugsum  21182  madurid  21183  cpmat  21247  pmatcollpwfi  21320  pmatcollpw3fi1lem1  21324  pm2mpval  21333  mp2pm2mplem5  21348  chpmat1dlem  21373  chpmat1d  21374  chpidmat  21385  cpmidpmat  21411  cpmadugsumfi  21415  chcoeffeqlem  21423  cayleyhamilton0  21427  cayleyhamiltonALT  21429  cayleyhamilton1  21430  restin  21704  imacmp  21935  conncompconn  21970  uptx  22163  cnpflf2  22538  tmdgsum2  22634  tsmsres  22681  tsmsf1o  22682  tsmsmhm  22683  prdsxmet  22908  resspwsds  22911  prdsxmslem2  23068  tngngpim  23197  metdcn2  23376  metdcn  23377  metdscn2  23394  iimulcn  23471  icchmeo  23474  xrhmeo  23479  cnrehmeo  23486  cnheiborlem  23487  evth  23492  evth2  23493  lebnumlem2  23495  reparphti  23530  pcoass  23557  pi1xfrcnv  23590  ipcau2  23766  ehl0base  23948  minveclem4  23964  pjthlem1  23969  ovolunlem1a  24026  unmbl  24067  uniioombl  24119  iblitg  24298  dfitg  24299  itg0  24309  iblcnlem1  24317  itgcnlem  24319  itgabs  24364  limcdif  24403  limccnp  24418  limccnp2  24419  dvexp  24479  dvmptid  24483  dvmptc  24484  dvmptfsum  24501  dveflem  24505  dvsincos  24507  mvth  24518  dvlipcn  24520  dvivthlem1  24534  dvfsumle  24547  dvfsumlem2  24553  itgsubst  24575  tdeglem4  24583  tdeglem2  24584  plypf1  24731  plymullem1  24733  coesub  24776  dgrmulc  24790  fta1lem  24825  vieta1lem1  24828  vieta1lem2  24829  aalioulem4  24853  aaliou3lem3  24862  abelthlem2  24949  abelthlem8  24956  abelthlem9  24957  sinhalfpilem  24978  efhalfpi  24986  cospi  24987  efipi  24988  sin2pi  24990  cos2pi  24991  ef2pi  24992  sin2pim  25000  cos2pim  25001  sinmpi  25002  cosmpi  25003  sinppi  25004  cosppi  25005  sincosq4sgn  25016  tangtx  25020  sincos4thpi  25028  sincos6thpi  25030  sincos3rdpi  25031  pige3ALT  25034  abssinper  25035  efif1olem4  25056  efifo  25058  eff1o  25060  circgrp  25063  circsubm  25064  logneg  25098  logimul  25124  logneg2  25125  dvrelog  25147  logcnlem4  25155  dvlog  25161  dvlog2  25163  logtayl  25170  1cxp  25182  ecxp  25183  cxpsqrt  25213  2irrexpq  25240  dvsqrt  25250  dvcnsqrt  25252  root1eq1  25263  cxpeq  25265  elogb  25275  2logb9irrALT  25303  ang180lem1  25314  ang180lem2  25315  heron  25343  1cubrlem  25346  1cubr  25347  dcubic2  25349  mcubic  25352  cubic2  25353  binom4  25355  dquartlem1  25356  dquartlem2  25357  dquart  25358  quart1lem  25360  quart1  25361  quartlem1  25362  asinsin  25397  asin1  25399  acos1  25400  atanlogsublem  25420  atanlogsub  25421  efiatan2  25422  2efiatan  25423  tanatan  25424  atanbnd  25431  atan1  25433  dvatan  25440  atantayl2  25443  leibpilem2  25447  leibpi  25448  log2cnv  25450  log2tlbnd  25451  log2ublem1  25452  log2ublem2  25453  log2ublem3  25454  log2ub  25455  birthday  25460  amgmlem  25495  emcllem5  25505  lgamgulmlem2  25535  lgamgulmlem5  25538  lgam1  25569  wilthlem2  25574  ftalem6  25583  basellem2  25587  basellem3  25588  basellem5  25590  basellem8  25593  cht1  25670  chp1  25672  1sgmprm  25703  ppiublem2  25707  ppiub  25708  chtublem  25715  chtub  25716  logfacbnd3  25727  bcp1ctr  25783  bclbnd  25784  bposlem4  25791  bposlem6  25793  bposlem8  25795  bposlem9  25796  lgslem1  25801  lgsdir2lem1  25829  lgsdir2lem2  25830  lgsdir2lem3  25831  lgsdir2lem5  25833  lgs1  25845  gausslemma2dlem1a  25869  gausslemma2dlem3  25872  gausslemma2dlem4  25873  gausslemma2d  25878  lgseisenlem1  25879  lgseisenlem3  25881  lgsquadlem1  25884  lgsquadlem2  25885  lgsquad2lem2  25889  m1lgs  25892  2lgslem1a2  25894  2sqlem8  25930  2sqblem  25935  addsq2nreurex  25948  logdivsum  26037  mulog2sumlem2  26039  log2sumbnd  26048  selberglem1  26049  selberglem2  26050  pntrmax  26068  pntibndlem2  26095  pntibndlem3  26096  pntlemg  26102  pntlemr  26106  pntlemo  26111  ostth2lem3  26139  ostth2lem4  26140  istrkg3ld  26175  trgcgrg  26229  tgcgr4  26245  colperpexlem1  26444  ax5seglem7  26649  axlowdimlem16  26671  setsiedg  26749  vdegp1ci  27248  finsumvtxdg2sstep  27259  finsumvtxdg2size  27260  wlkp1lem6  27388  wlkp1lem8  27390  wlkp1  27391  uhgrwkspthlem2  27463  pthdlem1  27475  pthdlem2  27477  pthd  27478  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  crctcshwlkn0lem6  27521  crctcshlem4  27526  crctcshwlkn0  27527  2wlkdlem2  27633  2wlkdlem4  27635  2pthdlem1  27637  wwlks2onv  27660  clwlkclwwlk2  27709  clwwlkwwlksb  27761  wwlksext2clwwlk  27764  clwwlknonex2lem1  27814  0ewlk  27821  1ewlk  27822  0wlk  27823  1pthdlem1  27842  1pthdlem2  27843  1wlkdlem1  27844  1wlkdlem4  27847  wlk2v2e  27864  3wlkdlem2  27867  3wlkdlem4  27869  3pthdlem1  27871  eupth0  27921  eupthp1  27923  eucrctshift  27950  eucrct2eupth  27952  numclwwlk1lem2foalem  28058  numclwlk2lem2f  28084  frgrregord013  28102  ex-exp  28157  ex-bc  28159  ex-gcd  28164  ex-lcm  28165  ex-ind-dvds  28168  smcnlem  28402  ipidsq  28415  dipcj  28419  dip0r  28422  nmlnoubi  28501  nmblolbii  28504  blocnilem  28509  ip1ilem  28531  ip2i  28533  ipdirilem  28534  ipasslem10  28544  ipasslem11  28545  siilem1  28556  hvmul0  28729  hvsubsub4i  28764  hvnegdii  28767  hvsubeq0i  28768  hvsubcan2i  28769  hvsubaddi  28771  hvsub0  28781  hisubcomi  28809  normlem0  28814  normlem1  28815  normlem2  28816  normlem3  28817  normlem9  28823  norm-ii-i  28842  norm3difi  28852  normpari  28859  polid2i  28862  polidi  28863  bcsiALT  28884  pjhthlem1  29096  chdmm3i  29184  chdmm4i  29185  chjidm  29225  chj4i  29228  chjjdiri  29229  spanunsni  29284  pjoml4i  29292  cmcm2i  29298  qlax4i  29335  qlax5i  29336  pjadjii  29379  pjmulii  29382  pjsubii  29383  pjssmii  29386  pjcji  29389  pjneli  29428  hoadd32i  29483  ho0subi  29500  hosubid1  29503  hosd2i  29528  hopncani  29529  hosubeq0i  29531  lnopeq0lem1  29710  lnopunilem1  29715  lnophmlem2  29722  nmbdoplbi  29729  nmcopexi  29732  lnfnmuli  29749  nmcfnexi  29756  nmoptri2i  29804  nmopcoadji  29806  golem1  29976  mdsl1i  30026  cvmdi  30029  mdslmd3i  30037  csmdsymi  30039  dfdec100  30474  dp20u  30482  dpmul10  30499  dpmul100  30501  dp3mul10  30502  dpmul1000  30503  dpexpp1  30512  0dp2dp  30513  dpmul  30517  dpmul4  30518  1mhdrd  30520  s2rn  30548  s3rn  30550  s3f1  30551  cshw1s2  30562  xrge00  30601  gsummpt2co  30614  gsumle  30653  psgnfzto1st  30675  cyc2fv1  30691  cycpmco2lem5  30700  cycpmco2lem6  30701  cycpmco2  30703  cyc3fv1  30707  cyc3fv2  30708  archirngz  30746  archiabllem2c  30752  gsumvsca1  30782  gsumvsca2  30783  xrge0slmod  30845  fply1  30859  lbsdiflsp0  30922  fedgmul  30927  ccfldextrr  30938  lmat22det  30987  madjusmdetlem4  30995  raddcn  31072  xrge0iifhom  31080  xrge0mulc1cn  31084  cbvesum  31201  gsumesum  31218  esumpfinvallem  31233  esumpfinvalf  31235  dya2icoseg  31435  sitg0  31504  eulerpartlemd  31524  eulerpartlemgvv  31534  eulerpartlemgh  31536  fib0  31557  fib1  31558  fibp1  31559  orrvcval4  31622  orrvcoel  31623  orrvccel  31624  coinflipprob  31637  coinflippvt  31642  ballotlem2  31646  ballotth  31695  signstf0  31738  signstfvn  31739  signsvtn0  31740  signstfvp  31741  signstfveq0  31747  signsvf0  31750  signsvf1  31751  signsvfn  31752  prodfzo03  31774  itgexpif  31777  repr0  31782  hgt750lemd  31819  hgt750lem  31822  hgt750lem2  31823  subfacp1lem1  32324  subfacp1lem5  32329  subfacval2  32332  subfaclim  32333  subfacval3  32334  cvxpconn  32387  cvxsconn  32388  sate0  32560  mrsub0  32661  problem4  32809  quad3  32811  sinccvglem  32813  iexpire  32865  faclimlem1  32873  fprlem1  33035  frrlem15  33040  fwddifnp1  33524  knoppcnlem10  33739  knoppndvlem7  33755  knoppndvlem21  33769  cnndvlem1  33774  finxpreclem4  34558  ptrest  34773  poimirlem27  34801  dvtan  34824  itgabsnc  34843  ftc1anclem8  34856  dvasin  34860  dvacos  34861  areacirclem1  34864  areacirclem4  34867  areacirc  34869  prdstotbnd  34955  prdsbnd2  34956  repwsmet  34995  rrnequiv  34996  reheibor  35000  dalem-cly  36689  pmodN  36868  cdleme0cp  37232  cdleme0cq  37233  cdleme1  37245  cdleme3d  37249  cdleme3h  37253  cdleme4  37256  cdleme5  37258  cdleme7a  37261  cdleme8  37268  cdleme9  37271  cdleme10  37272  cdleme11g  37283  cdleme15b  37293  cdleme21  37355  cdleme22e  37362  cdleme22eALTN  37363  cdleme23c  37369  cdleme25cv  37376  cdleme35b  37468  cdleme35c  37469  cdleme42a  37489  cdleme42d  37491  cdleme43aN  37507  cdlemeg46gfv  37548  cdlemk35  37930  dihjatcclem1  38436  lcdval2  38608  mapdpglem21  38710  sqsumi  39047  sqmid3api  39049  sqn5ii  39052  sq3deccom12  39056  re1m1e0m0  39107  sn-00idlem1  39108  remul02  39115  resubid  39118  mapfzcons  39193  mapfzcons1cl  39195  2rexfrabdioph  39273  3rexfrabdioph  39274  4rexfrabdioph  39275  6rexfrabdioph  39276  7rexfrabdioph  39277  rabdiophlem2  39279  diophren  39290  rabren3dioph  39292  pellexlem5  39310  pell1qr1  39348  rmspecfund  39386  jm2.17a  39437  jm2.17b  39438  jm2.27c  39484  jm2.27dlem5  39490  lmhmlnmsplit  39567  arearect  39702  areaquad  39703  relexp2  39902  trclfvdecomr  39953  k0004val0  40384  inductionexd  40385  unitadd  40429  amgm2d  40432  amgm3d  40433  lhe4.4ex1a  40541  expgrowthi  40545  expgrowth  40547  bccn1  40556  binomcxplemdvbinom  40565  binomcxplemdvsum  40567  binomcxplemnotnn0  40568  binomcxp  40569  refsumcn  41167  unirnmapsn  41357  oddfl  41423  infleinflem2  41519  sumnnodd  41791  cosnegpi  42028  dvcosre  42076  dvsinax  42077  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvmptmulf  42102  dvxpaek  42105  dvmptfprod  42110  dvnprodlem2  42112  dvnprodlem3  42113  itgsin0pilem1  42115  itgsinexplem1  42119  itgsubsticclem  42140  stoweidlem13  42179  wallispilem4  42234  wallispi2lem1  42237  wallispi2lem2  42238  stirlinglem1  42240  dirkerper  42262  dirkertrigeqlem1  42264  dirkertrigeqlem3  42266  dirkertrigeq  42267  dirkeritg  42268  dirkercncflem1  42269  dirkercncflem2  42270  fourierdlem36  42309  fourierdlem41  42314  fourierdlem42  42315  fourierdlem48  42320  fourierdlem56  42328  fourierdlem57  42329  fourierdlem58  42330  fourierdlem60  42332  fourierdlem61  42333  fourierdlem62  42334  fourierdlem65  42337  fourierdlem73  42345  fourierdlem80  42352  fourierdlem87  42359  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem100  42372  fourierdlem103  42375  fourierdlem107  42379  fourierdlem112  42384  fourierdlem113  42385  fourierdlem115  42387  fouriercnp  42392  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  etransclem2  42402  etransclem37  42437  etransclem46  42446  hoidmvlelem3  42760  vonioolem2  42844  issmflem  42885  smfmullem2  42948  simpcntrab  43008  1t10e1p1e11  43391  fmtno0  43549  fmtno1  43550  fmtnorec2lem  43551  fmtnorec3  43557  fmtno2  43559  fmtno3  43560  fmtno4  43561  fmtno4sqrt  43580  fmtno4prmfac  43581  2exp5  43602  139prmALT  43606  31prm  43607  2exp7  43609  2exp11  43612  mod42tp1mod8  43614  lighneallem2  43618  5tcu2e40  43627  3exp4mod41  43628  41prothprmlem1  43629  41prothprmlem2  43630  41prothprm  43631  bits0ALTV  43691  fppr2odd  43743  341fppr2  43746  4fppr1  43747  9fppr8  43749  sbgoldbo  43799  nnsum3primes4  43800  nnsum3primesgbe  43804  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  bgoldbtbndlem1  43817  tgoldbachlt  43828  2t6m3t4e0  44294  zlmodzxzequa  44449  zlmodzxznm  44450  zlmodzxzequap  44452  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  nn0sumshdiglem1  44579  prelrrx2  44598  prelrrx2b  44599  2sphere  44634  line2  44637  itsclquadb  44661  itscnhlinecirc02plem3  44669  inlinecirc02p  44672  sec0  44757  amgmw2d  44803
  Copyright terms: Public domain W3C validator