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

Theorem fveq2 5178
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 3767 . . 3  |-  ( A  =  B  ->  ( A F x  <->  B F x ) )
21iotabidv 4888 . 2  |-  ( A  =  B  ->  ( iota x A F x )  =  ( iota
x B F x ) )
3 df-fv 4910 . 2  |-  ( F `
 A )  =  ( iota x A F x )
4 df-fv 4910 . 2  |-  ( F `
 B )  =  ( iota x B F x )
52, 3, 43eqtr4g 2097 1  |-  ( A  =  B  ->  ( F `  A )  =  ( F `  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243   class class class wbr 3764   iotacio 4865   ` cfv 4902
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910
This theorem is referenced by:  fveq2i  5181  fveq2d  5182  dffn5imf  5228  fvelimab  5229  ssimaex  5234  fvmptssdm  5255  fvmptf  5263  eqfnfv2f  5269  fvelrn  5298  ralrnmpt  5309  rexrnmpt  5310  foco2  5318  ffnfvf  5324  fmptco  5330  fcompt  5333  fcoconst  5334  fnressn  5349  fressnfv  5350  fconstfvm  5379  funiunfvdmf  5403  f1veqaeq  5408  dff13f  5409  f1fveq  5411  f1elima  5412  f1ocnvfv  5419  f1ocnvfvb  5420  fcofo  5424  cocan2  5428  fliftfun  5436  isorel  5448  isocnv  5451  isotr  5456  f1oiso2  5466  ffnov  5605  eqfnov  5607  fnovim  5609  fnrnov  5646  foov  5647  funimassov  5650  ovelimab  5651  suppssfv  5708  fnofval  5721  ofrval  5722  offval2  5726  ofrfval2  5727  ofco  5729  caofinvl  5733  op1std  5775  op2ndd  5776  1stval2  5782  2ndval2  5783  unielxp  5800  reldm  5812  oprabco  5838  2ndconst  5843  f1o2ndf1  5849  mpt2xopn0yelv  5854  mpt2xopoveq  5855  smoel  5915  tfrlem1  5923  tfrlem3-2  5927  tfrlem3-2d  5928  tfrlem5  5930  tfrlem9  5935  tfr0  5937  tfrlemiubacc  5944  tfrlemi1  5946  tfrexlem  5948  tfri3  5953  rdgtfr  5961  rdgss  5970  rdgisuc1  5971  rdgisucinc  5972  rdgon  5973  frecabex  5984  frecsuclem3  5990  frecsuc  5991  frecrdg  5992  freccl  5993  oav  6034  omv  6035  oeiv  6036  dom2lem  6252  xpcomco  6300  fidceq  6330  ordiso2  6355  mulpipq2  6467  genipv  6605  genpelxp  6607  addcanprleml  6710  addcanprlemu  6711  recexprlemm  6720  recexprlemdisj  6726  recexprlemloc  6727  recexprlem1ssl  6729  recexprlem1ssu  6730  cauappcvgprlemm  6741  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  cauappcvgprlem2  6756  cauappcvgprlemlim  6757  cauappcvgpr  6758  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemm  6764  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprlemcl  6772  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprlem1  6775  caucvgprlem2  6776  caucvgpr  6778  caucvgprprlemell  6781  caucvgprprlemelu  6782  caucvgprprlemcbv  6783  caucvgprprlemval  6784  caucvgprprlemnkeqj  6786  caucvgprprlemnbj  6789  caucvgprprlemml  6790  caucvgprprlemmu  6791  caucvgprprlemopl  6793  caucvgprprlemlol  6794  caucvgprprlemopu  6795  caucvgprprlemloc  6799  caucvgprprlemclphr  6801  caucvgprprlemexbt  6802  caucvgprprlem1  6805  caucvgprprlem2  6806  caucvgsrlemcl  6871  caucvgsrlemfv  6873  caucvgsrlembound  6876  caucvgsrlemgt1  6877  caucvgsrlemoffval  6878  caucvgsrlemoffres  6882  caucvgsrlembnd  6883  caucvgsr  6884  axcaucvglemcau  6970  axcaucvglemres  6971  uz11  8493  cnref1o  8580  fzprval  8942  fztpval  8943  frec2uzzd  9160  frec2uzuzd  9162  frec2uzltd  9163  frec2uzlt2d  9164  frecuzrdgrrn  9168  frec2uzrdg  9169  frecuzrdgfn  9172  frecfzennn  9177  iseqeq1  9188  iseqovex  9193  iseqval  9194  iseqfn  9195  iseq1  9196  iseqcl  9197  iseqp1  9199  iseqss  9200  iseqfveq2  9202  iseqfveq  9204  iseqfeq  9205  iseqshft2  9206  monoord  9209  monoord2  9210  isermono  9211  iseqsplit  9212  iseqcaopr3  9214  iseqcaopr2  9215  iseqid3s  9220  iseqhomo  9222  serile  9227  expivallem  9230  expival  9231  reval  9423  replim  9433  cj11  9479  caucvgre  9554  cvg1nlemcau  9557  cvg1nlemres  9558  rexuz3  9562  absval  9573  resqrexlemover  9582  resqrexlemdecn  9584  resqrexlemlo  9585  resqrexlemcalc3  9588  resqrexlemnm  9590  resqrexlemcvg  9591  resqrexlemoverl  9593  resqrexlemglsq  9594  resqrexlemga  9595  resqrexlemsqa  9596  resqrexlemex  9597  abs00bd  9638  cau3lem  9684  caubnd2  9687  climconst  9785  climmpt  9795  climshftlemg  9797  climcn1  9803  climle  9828  climub  9838  climserile  9839  climcau  9840  climcvg1nlem  9842  climcvg1n  9843  serif0  9845  nn0seqcvgd  9854  ialginv  9860  ialgcvg  9861  ialgcvga  9864  ialgfx  9865  qdencn  10097
  Copyright terms: Public domain W3C validator