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

Theorem fveq2 5178
Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
fveq2 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))

Proof of Theorem fveq2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 breq1 3767 . . 3 (𝐴 = 𝐵 → (𝐴𝐹𝑥𝐵𝐹𝑥))
21iotabidv 4888 . 2 (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3 df-fv 4910 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 4910 . 2 (𝐹𝐵) = (℩𝑥𝐵𝐹𝑥)
52, 3, 43eqtr4g 2097 1 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243   class class class wbr 3764  cio 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  6357  mulpipq2  6469  genipv  6607  genpelxp  6609  addcanprleml  6712  addcanprlemu  6713  recexprlemm  6722  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  cauappcvgprlemm  6743  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlem2  6758  cauappcvgprlemlim  6759  cauappcvgpr  6760  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgprlem2  6778  caucvgpr  6780  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnkeqj  6788  caucvgprprlemnbj  6791  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgprprlem1  6807  caucvgprprlem2  6808  caucvgsrlemcl  6873  caucvgsrlemfv  6875  caucvgsrlembound  6878  caucvgsrlemgt1  6879  caucvgsrlemoffval  6880  caucvgsrlemoffres  6884  caucvgsrlembnd  6885  caucvgsr  6886  axcaucvglemcau  6972  axcaucvglemres  6973  uz11  8495  cnref1o  8582  fzprval  8944  fztpval  8945  frec2uzzd  9186  frec2uzuzd  9188  frec2uzltd  9189  frec2uzlt2d  9190  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgfn  9198  frecfzennn  9203  iseqeq1  9214  iseqovex  9219  iseqval  9220  iseqfn  9221  iseq1  9222  iseqcl  9223  iseqp1  9225  iseqss  9226  iseqfveq2  9228  iseqfveq  9230  iseqfeq  9231  iseqshft2  9232  monoord  9235  monoord2  9236  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseqid3s  9246  iseqhomo  9248  serile  9253  expivallem  9256  expival  9257  reval  9449  replim  9459  cj11  9505  caucvgre  9580  cvg1nlemcau  9583  cvg1nlemres  9584  rexuz3  9588  absval  9599  resqrexlemover  9608  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  resqrexlemsqa  9622  resqrexlemex  9623  abs00bd  9664  cau3lem  9710  caubnd2  9713  climconst  9811  climmpt  9821  climshftlemg  9823  climcn1  9829  climle  9854  climub  9864  climserile  9865  climcau  9866  climcvg1nlem  9868  climcvg1n  9869  serif0  9871  nn0seqcvgd  9880  ialginv  9886  ialgcvg  9887  ialgcvga  9890  ialgfx  9891  qdencn  10124
  Copyright terms: Public domain W3C validator