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

Theorem fveq2 5268
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 3823 . . 3 (𝐴 = 𝐵 → (𝐴𝐹𝑥𝐵𝐹𝑥))
21iotabidv 4967 . 2 (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3 df-fv 4989 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 4989 . 2 (𝐹𝐵) = (℩𝑥𝐵𝐹𝑥)
52, 3, 43eqtr4g 2142 1 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287   class class class wbr 3820  cio 4944  cfv 4981
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-br 3821  df-iota 4946  df-fv 4989
This theorem is referenced by:  fveq2i  5271  fveq2d  5272  2fveq3  5273  fvifdc  5290  dffn5imf  5322  fvelimab  5323  ssimaex  5328  fvco4  5339  fvmptssdm  5350  fvmptf  5358  eqfnfv2f  5364  fvelrn  5393  ralrnmpt  5404  rexrnmpt  5405  ffnfvf  5420  fmptco  5427  fcompt  5430  fcoconst  5431  fnressn  5446  fressnfv  5447  fconstfvm  5476  foco2  5494  funiunfvdmf  5504  f1veqaeq  5509  dff13f  5510  f1fveq  5512  f1elima  5513  f1ocnvfv  5519  f1ocnvfvb  5520  fcofo  5524  cocan2  5528  fliftfun  5536  isorel  5548  isocnv  5551  isotr  5556  f1oiso2  5567  ffnov  5706  eqfnov  5708  fnovim  5710  fnrnov  5747  foov  5748  funimassov  5751  ovelimab  5752  suppssfv  5809  fnofval  5822  ofrval  5823  offval2  5827  ofrfval2  5828  ofco  5830  caofinvl  5834  op1std  5876  op2ndd  5877  1stval2  5883  2ndval2  5884  unielxp  5901  reldm  5913  oprabco  5939  2ndconst  5944  f1o2ndf1  5950  mpt2xopn0yelv  5958  mpt2xopoveq  5959  smoel  6019  tfrlem1  6027  tfrlem3-2d  6031  tfrlem5  6033  tfrlem9  6038  tfr0dm  6041  tfrlemiubacc  6049  tfrlemi1  6051  tfrexlem  6053  tfr1onlemsucfn  6059  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfr1onlemubacc  6065  tfr1onlemaccex  6067  tfr1onlemres  6068  tfri1dALT  6070  tfrcllemsucfn  6072  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemubacc  6078  tfrcllemaccex  6080  tfrcllemres  6081  tfrcldm  6082  tfrcl  6083  tfri3  6086  rdgtfr  6093  rdgss  6102  rdgisuc1  6103  rdgisucinc  6104  rdgon  6105  frecabex  6117  frecabcl  6118  frecfcllem  6123  frecsuclem  6125  frecsuc  6126  frecrdg  6127  oav  6169  omv  6170  oeiv  6171  dom2lem  6441  xpcomco  6494  xpmapen  6518  fidceq  6537  ordiso2  6672  djur  6701  djune  6713  updjudhcoinlf  6715  updjudhcoinrg  6716  updjud  6717  enomnilem  6738  finomni  6740  fodjuomnilemdc  6743  fodjuomnilemm  6745  fodjuomnilem0  6746  fodjuomnilemres  6747  fodjuomni  6748  mulpipq2  6874  genipv  7012  genpelxp  7014  addcanprleml  7117  addcanprlemu  7118  recexprlemm  7127  recexprlemdisj  7133  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  cauappcvgprlemm  7148  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  cauappcvgprlem2  7163  cauappcvgprlemlim  7164  cauappcvgpr  7165  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem1  7182  caucvgprlem2  7183  caucvgpr  7185  caucvgprprlemell  7188  caucvgprprlemelu  7189  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemnkeqj  7193  caucvgprprlemnbj  7196  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlemclphr  7208  caucvgprprlemexbt  7209  caucvgprprlem1  7212  caucvgprprlem2  7213  caucvgsrlemcl  7278  caucvgsrlemfv  7280  caucvgsrlembound  7283  caucvgsrlemgt1  7284  caucvgsrlemoffval  7285  caucvgsrlemoffres  7289  caucvgsrlembnd  7290  caucvgsr  7291  axcaucvglemcau  7377  axcaucvglemres  7378  uz11  8973  cnref1o  9065  fzprval  9426  fztpval  9427  frec2uzuzd  9737  frec2uzltd  9738  frec2uzlt2d  9739  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgtcl  9747  frecuzrdgg  9751  frecuzrdgfunlem  9754  frecfzennn  9761  iseqeq1  9782  iseqovex  9787  iseqval  9788  iseqvalt  9790  iseq1  9791  iseq1t  9792  iseqfcl  9793  iseqfclt  9794  iseqcl  9795  iseqp1  9796  iseqp1t  9797  iseqoveq  9798  iseqss  9799  iseqsst  9800  iseqfveq2  9802  iseqfveq  9804  iseqfeq  9805  iseqshft2  9806  monoord  9809  monoord2  9810  isermono  9811  iseqsplit  9812  iseqcaopr3  9814  iseqcaopr2  9815  iseqf1olemkle  9817  iseqf1olemklt  9818  iseqf1olemqval  9820  iseqf1olemqk  9827  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemfvp  9830  iseqf1olemqsumkj  9831  iseqf1olemqsum  9833  iseqf1olemstep  9834  iseqf1olemp  9835  iseqf1oleml  9836  iseqf1o  9837  iseqid3s  9841  iseqid2  9843  iseqhomo  9844  iseqz  9845  serile  9851  expivallem  9854  expival  9855  facp1  10034  faccl  10039  facdiv  10042  facwordi  10044  faclbnd  10045  facubnd  10049  bcval  10053  ibcval5  10067  fz1eqb  10095  omgadd  10106  hashxp  10130  zfz1isolem1  10141  zfz1iso  10142  iseqcoll  10143  reval  10178  replim  10188  cj11  10234  caucvgre  10309  cvg1nlemcau  10312  cvg1nlemres  10313  rexuz3  10318  absval  10329  resqrexlemover  10338  resqrexlemdecn  10340  resqrexlemlo  10341  resqrexlemcalc3  10344  resqrexlemnm  10346  resqrexlemcvg  10347  resqrexlemoverl  10349  resqrexlemglsq  10350  resqrexlemga  10351  resqrexlemsqa  10352  resqrexlemex  10353  abs00bd  10394  cau3lem  10442  caubnd2  10445  climconst  10571  climmpt  10581  climshftlemg  10583  climcn1  10589  climle  10614  climub  10624  climserile  10625  climcau  10626  climcvg1nlem  10628  climcvg1n  10629  serif0  10631  fisumcvg  10656  isummolem3  10659  isummolem2a  10660  isummolem2  10661  isummo  10662  zisum  10663  fisum  10665  fsumf1o  10668  fisumss  10670  dvdsabseq  10723  dvdsfac  10736  zsupcllemex  10817  infssuzex  10820  gcd0id  10845  nn0seqcvgd  10898  ialginv  10904  ialgcvg  10905  ialgcvga  10908  ialgfx  10909  eucalglt  10914  lcmid  10937  qredeu  10954  prmfac1  11006  sqne2sq  11030  qnumdenbi  11045  dfphi2  11071  nnsf  11333  nninfalllemn  11336  nninfalllem1  11337  nninfomnilem  11348  qdencn  11353
  Copyright terms: Public domain W3C validator