ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fveq2 Unicode version

Theorem fveq2 5389
Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
fveq2  |-  ( A  =  B  ->  ( F `  A )  =  ( F `  B ) )

Proof of Theorem fveq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 breq1 3902 . . 3  |-  ( A  =  B  ->  ( A F x  <->  B F x ) )
21iotabidv 5079 . 2  |-  ( A  =  B  ->  ( iota x A F x )  =  ( iota
x B F x ) )
3 df-fv 5101 . 2  |-  ( F `
 A )  =  ( iota x A F x )
4 df-fv 5101 . 2  |-  ( F `
 B )  =  ( iota x B F x )
52, 3, 43eqtr4g 2175 1  |-  ( A  =  B  ->  ( F `  A )  =  ( F `  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316   class class class wbr 3899   iotacio 5056   ` cfv 5093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101
This theorem is referenced by:  fveq2i  5392  fveq2d  5393  2fveq3  5394  fvifdc  5411  dffn5imf  5444  fvelimab  5445  ssimaex  5450  fvco4  5461  fvmptssdm  5473  fvmptf  5481  eqfnfv2f  5490  fvelrn  5519  ralrnmpt  5530  rexrnmpt  5531  ffnfvf  5547  fmptco  5554  cofmpt  5557  fcompt  5558  fcoconst  5559  fnressn  5574  fressnfv  5575  fconstfvm  5606  foco2  5623  funiunfvdmf  5633  f1veqaeq  5638  dff13f  5639  f1fveq  5641  f1elima  5642  f1ocnvfv  5648  f1ocnvfvb  5649  fcofo  5653  cocan2  5657  fliftfun  5665  isorel  5677  isocnv  5680  isotr  5685  f1oiso2  5696  imbrov2fvoveq  5767  ffnov  5843  eqfnov  5845  fnovim  5847  fnrnov  5884  foov  5885  funimassov  5888  ovelimab  5889  suppssfv  5946  ofvalg  5959  ofrval  5960  offval2  5965  ofrfval2  5966  ofco  5968  caofinvl  5972  op1std  6014  op2ndd  6015  1stval2  6021  2ndval2  6022  unielxp  6040  reldm  6052  oprabco  6082  2ndconst  6087  f1o2ndf1  6093  mpoxopn0yelv  6104  mpoxopoveq  6105  smoel  6165  tfrlem1  6173  tfrlem3-2d  6177  tfrlem5  6179  tfrlem9  6184  tfr0dm  6187  tfrlemiubacc  6195  tfrlemi1  6197  tfrexlem  6199  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemubacc  6211  tfr1onlemaccex  6213  tfr1onlemres  6214  tfri1dALT  6216  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemubacc  6224  tfrcllemaccex  6226  tfrcllemres  6227  tfrcldm  6228  tfrcl  6229  tfri3  6232  rdgtfr  6239  rdgss  6248  rdgisuc1  6249  rdgisucinc  6250  rdgon  6251  frecabex  6263  frecabcl  6264  frecfcllem  6269  frecsuclem  6271  frecsuc  6272  frecrdg  6273  oav  6318  omv  6319  oeiv  6320  fvixp  6565  cbvixp  6577  mptelixpg  6596  elixpsn  6597  dom2lem  6634  xpcomco  6688  xpmapen  6712  fidceq  6731  fieq0  6832  ordiso2  6888  djune  6931  updjudhcoinlf  6933  updjudhcoinrg  6934  updjud  6935  omp1eom  6948  0ct  6960  ctmlemr  6961  ctssdclemn0  6963  ctssdccl  6964  ctssdc  6966  enumctlemm  6967  enomnilem  6978  finomni  6980  fodjuomnilemdc  6984  fodju0  6987  fodjuomni  6989  ismkvnex  6997  fodjumkv  7002  exmidaclem  7032  mulpipq2  7147  genipv  7285  genpelxp  7287  addcanprleml  7390  addcanprlemu  7391  recexprlemm  7400  recexprlemdisj  7406  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  cauappcvgprlemm  7421  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlem2  7436  cauappcvgprlemlim  7437  cauappcvgpr  7438  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgprlem2  7456  caucvgpr  7458  caucvgprprlemell  7461  caucvgprprlemelu  7462  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemnkeqj  7466  caucvgprprlemnbj  7469  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemloc  7479  caucvgprprlemclphr  7481  caucvgprprlemexbt  7482  caucvgprprlem1  7485  caucvgprprlem2  7486  caucvgsrlemcl  7565  caucvgsrlemfv  7567  caucvgsrlembound  7570  caucvgsrlemgt1  7571  caucvgsrlemoffval  7572  caucvgsrlemoffres  7576  caucvgsrlembnd  7577  caucvgsr  7578  axcaucvglemcau  7674  axcaucvglemres  7675  uz11  9316  cnref1o  9408  fzprval  9830  fztpval  9831  frec2uzuzd  10143  frec2uzltd  10144  frec2uzlt2d  10145  frecuzrdgrrn  10149  frec2uzrdg  10150  frecuzrdgtcl  10153  frecuzrdgg  10157  frecuzrdgfunlem  10160  frecfzennn  10167  seqeq1  10189  iseqovex  10197  seq3val  10199  seqvalcd  10200  seq3-1  10201  seqf  10202  seq3p1  10203  seqovcd  10204  seqp1cd  10207  seq3clss  10208  seq3fveq2  10210  seq3fveq  10212  seq3feq  10213  seq3shft2  10214  monoord  10217  monoord2  10218  ser3mono  10219  seq3split  10220  seq3caopr3  10222  seq3caopr2  10223  iseqf1olemkle  10225  iseqf1olemklt  10226  iseqf1olemqval  10228  iseqf1olemqk  10235  iseqf1olemjpcl  10236  iseqf1olemqpcl  10237  iseqf1olemfvp  10238  seq3f1olemqsumkj  10239  seq3f1olemqsum  10241  seq3f1olemstep  10242  seq3f1olemp  10243  seq3f1oleml  10244  seq3f1o  10245  seq3id2  10250  seq3homo  10251  seq3z  10252  ser3ge0  10258  ser3le  10259  exp3vallem  10262  exp3val  10263  facp1  10444  faccl  10449  facdiv  10452  facwordi  10454  faclbnd  10455  facubnd  10459  bcval  10463  bcval5  10477  fz1eqb  10505  omgadd  10516  hashxp  10540  zfz1isolem1  10551  zfz1iso  10552  seq3coll  10553  seq3shft  10578  reval  10589  replim  10599  cj11  10645  caucvgre  10721  cvg1nlemcau  10724  cvg1nlemres  10725  rexuz3  10730  absval  10741  resqrexlemover  10750  resqrexlemdecn  10752  resqrexlemlo  10753  resqrexlemcalc3  10756  resqrexlemnm  10758  resqrexlemcvg  10759  resqrexlemoverl  10761  resqrexlemglsq  10762  resqrexlemga  10763  resqrexlemsqa  10764  resqrexlemex  10765  abs00bd  10806  cau3lem  10854  caubnd2  10857  climconst  11027  climmpt  11037  climshftlemg  11039  climcn1  11045  climle  11071  climub  11081  climserle  11082  climcau  11084  climcvg1nlem  11086  climcvg1n  11087  serf0  11089  fsum3cvg  11114  summodclem3  11117  summodclem2a  11118  summodclem2  11119  summodc  11120  zsumdc  11121  fsum3  11124  fsumf1o  11127  fisumss  11129  fsum3cvg2  11131  fsum3ser  11134  fsumcl2lem  11135  fsumadd  11143  sumsnf  11146  isummulc2  11163  isumge0  11167  isumadd  11168  fsum2dlemstep  11171  fsummulc2  11185  fsumconst  11191  fsumrelem  11208  isumshft  11227  isum1p  11229  isumnn0nn  11230  isumrpcl  11231  isumlessdc  11233  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  cvgratnnlemseq  11263  cvgratnnlemabsle  11264  cvgratnnlemfm  11266  cvgratnnlemrate  11267  cvgratnn  11268  cvgratz  11269  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  eftvalcn  11290  ef0lem  11293  ege2le3  11304  efcj  11306  efaddlem  11307  eftlub  11323  efgt1p2  11328  reef11  11333  tanvalap  11342  efieq1re  11405  eirraplem  11410  dvdsabseq  11472  dvdsfac  11485  zsupcllemex  11566  infssuzex  11569  gcd0id  11594  nn0seqcvgd  11649  alginv  11655  algcvg  11656  algcvga  11659  algfx  11660  eucalglt  11665  lcmid  11688  qredeu  11705  prmfac1  11757  sqne2sq  11782  qnumdenbi  11797  dfphi2  11823  ennnfonelemk  11840  ennnfonelemp1  11846  ennnfoneleminc  11851  ennnfonelemkh  11852  ennnfonelemhf1o  11853  ennnfonelemex  11854  ennnfonelemhom  11855  ennnfonelemrn  11859  ennnfonelemnn0  11862  ennnfonelemr  11863  ennnfonelemim  11864  ctinfomlemom  11867  ctinfom  11868  ctiunctlemfo  11879  sloteq  11891  topnvalg  12059  istps  12126  clsfval  12197  cnpval  12294  lmconst  12312  txcnp  12367  upxp  12368  uptx  12370  txlm  12375  lmcn2  12376  cnmpt11  12379  cnmpt11f  12380  cnmpt1t  12381  cnmpt21  12387  cnmpt21f  12388  cnmpt2t  12389  mopnval  12538  isxms  12547  isms  12549  comet  12595  mopnex  12601  xmetxp  12603  xmetxpbl  12604  txmetcnp  12614  txmetcn  12615  qtopbasss  12617  cncfi  12661  cncfmpt1f  12680  ivthinclemlm  12708  ivthinclemum  12709  ivthinclemlopn  12710  ivthinclemlr  12711  ivthinclemuopn  12712  ivthinclemur  12713  ivthinclemdisj  12714  ivthinclemloc  12715  ivthinc  12717  ivthdec  12718  cnlimci  12738  limccnpcntop  12740  eldvap  12747  dvcoapbr  12767  dvcj  12769  dvfre  12770  dveflem  12782  sin0pilem2  12790  pilem3  12791  coseq0q4123  12842  coseq0negpitopi  12844  subctctexmid  13123  nnsf  13126  nninfalllemn  13129  nninfalllem1  13130  nninfomnilem  13141  nninffeq  13143  qdencn  13149  isomninnlem  13152  trilpolemclim  13156  trilpolemcl  13157  trilpolemisumle  13158  trilpolemeq1  13160  trilpolemlt1  13161  trilpo  13163
  Copyright terms: Public domain W3C validator