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

Theorem fveq2 5209
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 3796 . . 3 (𝐴 = 𝐵 → (𝐴𝐹𝑥𝐵𝐹𝑥))
21iotabidv 4918 . 2 (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3 df-fv 4940 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 4940 . 2 (𝐹𝐵) = (℩𝑥𝐵𝐹𝑥)
52, 3, 43eqtr4g 2139 1 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285   class class class wbr 3793  cio 4895  cfv 4932
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940
This theorem is referenced by:  fveq2i  5212  fveq2d  5213  fvifdc  5228  dffn5imf  5260  fvelimab  5261  ssimaex  5266  fvmptssdm  5287  fvmptf  5295  eqfnfv2f  5301  fvelrn  5330  ralrnmpt  5341  rexrnmpt  5342  foco2  5350  ffnfvf  5356  fmptco  5362  fcompt  5365  fcoconst  5366  fnressn  5381  fressnfv  5382  fconstfvm  5411  funiunfvdmf  5435  f1veqaeq  5440  dff13f  5441  f1fveq  5443  f1elima  5444  f1ocnvfv  5450  f1ocnvfvb  5451  fcofo  5455  cocan2  5459  fliftfun  5467  isorel  5479  isocnv  5482  isotr  5487  f1oiso2  5497  ffnov  5636  eqfnov  5638  fnovim  5640  fnrnov  5677  foov  5678  funimassov  5681  ovelimab  5682  suppssfv  5739  fnofval  5752  ofrval  5753  offval2  5757  ofrfval2  5758  ofco  5760  caofinvl  5764  op1std  5806  op2ndd  5807  1stval2  5813  2ndval2  5814  unielxp  5831  reldm  5843  oprabco  5869  2ndconst  5874  f1o2ndf1  5880  mpt2xopn0yelv  5888  mpt2xopoveq  5889  smoel  5949  tfrlem1  5957  tfrlem3-2d  5961  tfrlem5  5963  tfrlem9  5968  tfr0dm  5971  tfrlemiubacc  5979  tfrlemi1  5981  tfrexlem  5983  tfr1onlemsucfn  5989  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemubacc  5995  tfr1onlemaccex  5997  tfr1onlemres  5998  tfri1dALT  6000  tfrcllemsucfn  6002  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemubacc  6008  tfrcllemaccex  6010  tfrcllemres  6011  tfrcldm  6012  tfrcl  6013  tfri3  6016  rdgtfr  6023  rdgss  6032  rdgisuc1  6033  rdgisucinc  6034  rdgon  6035  frecabex  6047  frecabcl  6048  frecfcllem  6053  frecsuclem  6055  frecsuc  6056  frecrdg  6057  oav  6098  omv  6099  oeiv  6100  dom2lem  6319  xpcomco  6370  fidceq  6404  ordiso2  6505  mulpipq2  6623  genipv  6761  genpelxp  6763  addcanprleml  6866  addcanprlemu  6867  recexprlemm  6876  recexprlemdisj  6882  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  cauappcvgprlemm  6897  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlem2  6912  cauappcvgprlemlim  6913  cauappcvgpr  6914  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem1  6931  caucvgprlem2  6932  caucvgpr  6934  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnkeqj  6942  caucvgprprlemnbj  6945  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlem1  6961  caucvgprprlem2  6962  caucvgsrlemcl  7027  caucvgsrlemfv  7029  caucvgsrlembound  7032  caucvgsrlemgt1  7033  caucvgsrlemoffval  7034  caucvgsrlemoffres  7038  caucvgsrlembnd  7039  caucvgsr  7040  axcaucvglemcau  7126  axcaucvglemres  7127  uz11  8722  cnref1o  8814  fzprval  9175  fztpval  9176  frec2uzuzd  9484  frec2uzltd  9485  frec2uzlt2d  9486  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgtcl  9494  frecuzrdgg  9498  frecuzrdgfunlem  9501  frecfzennn  9508  iseqeq1  9524  iseqovex  9529  iseqval  9530  iseqvalt  9532  iseq1  9533  iseq1t  9534  iseqfcl  9535  iseqfclt  9536  iseqcl  9537  iseqp1  9538  iseqp1t  9539  iseqoveq  9540  iseqss  9541  iseqsst  9542  iseqfveq2  9544  iseqfveq  9546  iseqfeq  9547  iseqshft2  9548  monoord  9551  monoord2  9552  isermono  9553  iseqsplit  9554  iseqcaopr3  9556  iseqcaopr2  9557  iseqid3s  9562  iseqid2  9564  iseqhomo  9565  iseqz  9566  serile  9571  expivallem  9574  expival  9575  facp1  9754  faccl  9759  facdiv  9762  facwordi  9764  faclbnd  9765  facubnd  9769  bcval  9773  ibcval5  9787  fz1eqb  9815  omgadd  9826  reval  9874  replim  9884  cj11  9930  caucvgre  10005  cvg1nlemcau  10008  cvg1nlemres  10009  rexuz3  10014  absval  10025  resqrexlemover  10034  resqrexlemdecn  10036  resqrexlemlo  10037  resqrexlemcalc3  10040  resqrexlemnm  10042  resqrexlemcvg  10043  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemga  10047  resqrexlemsqa  10048  resqrexlemex  10049  abs00bd  10090  cau3lem  10138  caubnd2  10141  climconst  10267  climmpt  10277  climshftlemg  10279  climcn1  10285  climle  10310  climub  10320  climserile  10321  climcau  10322  climcvg1nlem  10324  climcvg1n  10325  serif0  10327  fisumcvg  10338  dvdsabseq  10392  dvdsfac  10405  zsupcllemex  10486  infssuzex  10489  gcd0id  10514  nn0seqcvgd  10567  ialginv  10573  ialgcvg  10574  ialgcvga  10577  ialgfx  10578  eucalglt  10583  lcmid  10606  qredeu  10623  prmfac1  10675  sqne2sq  10699  qdencn  10943
  Copyright terms: Public domain W3C validator