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

Theorem fveq2 5428
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 3939 . . 3 (𝐴 = 𝐵 → (𝐴𝐹𝑥𝐵𝐹𝑥))
21iotabidv 5116 . 2 (𝐴 = 𝐵 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐵𝐹𝑥))
3 df-fv 5138 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 5138 . 2 (𝐹𝐵) = (℩𝑥𝐵𝐹𝑥)
52, 3, 43eqtr4g 2198 1 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332   class class class wbr 3936  cio 5093  cfv 5130
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-iota 5095  df-fv 5138
This theorem is referenced by:  fveq2i  5431  fveq2d  5432  2fveq3  5433  fvifdc  5450  dffn5imf  5483  fvelimab  5484  ssimaex  5489  fvco4  5500  fvmptssdm  5512  fvmptf  5520  eqfnfv2f  5529  fvelrn  5558  ralrnmpt  5569  rexrnmpt  5570  ffnfvf  5586  fmptco  5593  cofmpt  5596  fcompt  5597  fcoconst  5598  fnressn  5613  fressnfv  5614  fconstfvm  5645  foco2  5662  funiunfvdmf  5672  f1veqaeq  5677  dff13f  5678  f1fveq  5680  f1elima  5681  f1ocnvfv  5687  f1ocnvfvb  5688  fcofo  5692  cocan2  5696  fliftfun  5704  isorel  5716  isocnv  5719  isotr  5724  f1oiso2  5735  imbrov2fvoveq  5806  ffnov  5882  eqfnov  5884  fnovim  5886  fnrnov  5923  foov  5924  funimassov  5927  ovelimab  5928  suppssfv  5985  ofvalg  5998  ofrval  5999  offval2  6004  ofrfval2  6005  ofco  6007  caofinvl  6011  op1std  6053  op2ndd  6054  1stval2  6060  2ndval2  6061  unielxp  6079  reldm  6091  oprabco  6121  2ndconst  6126  f1o2ndf1  6132  mpoxopn0yelv  6143  mpoxopoveq  6144  smoel  6204  tfrlem1  6212  tfrlem3-2d  6216  tfrlem5  6218  tfrlem9  6223  tfr0dm  6226  tfrlemiubacc  6234  tfrlemi1  6236  tfrexlem  6238  tfr1onlemsucfn  6244  tfr1onlemsucaccv  6245  tfr1onlembxssdm  6247  tfr1onlembfn  6248  tfr1onlemubacc  6250  tfr1onlemaccex  6252  tfr1onlemres  6253  tfri1dALT  6255  tfrcllemsucfn  6257  tfrcllemsucaccv  6258  tfrcllembxssdm  6260  tfrcllembfn  6261  tfrcllemubacc  6263  tfrcllemaccex  6265  tfrcllemres  6266  tfrcldm  6267  tfrcl  6268  tfri3  6271  rdgtfr  6278  rdgss  6287  rdgisuc1  6288  rdgisucinc  6289  rdgon  6290  frecabex  6302  frecabcl  6303  frecfcllem  6308  frecsuclem  6310  frecsuc  6311  frecrdg  6312  oav  6357  omv  6358  oeiv  6359  fvixp  6604  cbvixp  6616  mptelixpg  6635  elixpsn  6636  dom2lem  6673  xpcomco  6727  xpmapen  6751  fidceq  6770  fieq0  6871  ordiso2  6927  djune  6970  updjudhcoinlf  6972  updjudhcoinrg  6973  updjud  6974  omp1eom  6987  0ct  6999  ctmlemr  7000  ctssdclemn0  7002  ctssdccl  7003  ctssdc  7005  enumctlemm  7006  enomnilem  7017  finomni  7019  fodjuomnilemdc  7023  fodju0  7026  fodjuomni  7028  ismkvnex  7036  fodjumkv  7041  exmidaclem  7080  cc1  7096  cc2lem  7097  cc2  7098  cc3  7099  mulpipq2  7202  genipv  7340  genpelxp  7342  addcanprleml  7445  addcanprlemu  7446  recexprlemm  7455  recexprlemdisj  7461  recexprlemloc  7462  recexprlem1ssl  7464  recexprlem1ssu  7465  cauappcvgprlemm  7476  cauappcvgprlemdisj  7482  cauappcvgprlemloc  7483  cauappcvgprlemladdru  7487  cauappcvgprlemladdrl  7488  cauappcvgprlem1  7490  cauappcvgprlem2  7491  cauappcvgprlemlim  7492  cauappcvgpr  7493  caucvgprlemnkj  7497  caucvgprlemnbj  7498  caucvgprlemm  7499  caucvgprlemdisj  7505  caucvgprlemloc  7506  caucvgprlemcl  7507  caucvgprlemladdfu  7508  caucvgprlemladdrl  7509  caucvgprlem1  7510  caucvgprlem2  7511  caucvgpr  7513  caucvgprprlemell  7516  caucvgprprlemelu  7517  caucvgprprlemcbv  7518  caucvgprprlemval  7519  caucvgprprlemnkeqj  7521  caucvgprprlemnbj  7524  caucvgprprlemml  7525  caucvgprprlemmu  7526  caucvgprprlemopl  7528  caucvgprprlemlol  7529  caucvgprprlemopu  7530  caucvgprprlemloc  7534  caucvgprprlemclphr  7536  caucvgprprlemexbt  7537  caucvgprprlem1  7540  caucvgprprlem2  7541  caucvgsrlemcl  7620  caucvgsrlemfv  7622  caucvgsrlembound  7625  caucvgsrlemgt1  7626  caucvgsrlemoffval  7627  caucvgsrlemoffres  7631  caucvgsrlembnd  7632  caucvgsr  7633  axcaucvglemcau  7729  axcaucvglemres  7730  uz11  9371  cnref1o  9468  fzprval  9892  fztpval  9893  frec2uzuzd  10205  frec2uzltd  10206  frec2uzlt2d  10207  frecuzrdgrrn  10211  frec2uzrdg  10212  frecuzrdgtcl  10215  frecuzrdgg  10219  frecuzrdgfunlem  10222  frecfzennn  10229  seqeq1  10251  iseqovex  10259  seq3val  10261  seqvalcd  10262  seq3-1  10263  seqf  10264  seq3p1  10265  seqovcd  10266  seqp1cd  10269  seq3clss  10270  seq3fveq2  10272  seq3fveq  10274  seq3feq  10275  seq3shft2  10276  monoord  10279  monoord2  10280  ser3mono  10281  seq3split  10282  seq3caopr3  10284  seq3caopr2  10285  iseqf1olemkle  10287  iseqf1olemklt  10288  iseqf1olemqval  10290  iseqf1olemqk  10297  iseqf1olemjpcl  10298  iseqf1olemqpcl  10299  iseqf1olemfvp  10300  seq3f1olemqsumkj  10301  seq3f1olemqsum  10303  seq3f1olemstep  10304  seq3f1olemp  10305  seq3f1oleml  10306  seq3f1o  10307  seq3id2  10312  seq3homo  10313  seq3z  10314  ser3ge0  10320  ser3le  10321  exp3vallem  10324  exp3val  10325  facp1  10507  faccl  10512  facdiv  10515  facwordi  10517  faclbnd  10518  facubnd  10522  bcval  10526  bcval5  10540  fz1eqb  10568  omgadd  10579  hashxp  10603  zfz1isolem1  10614  zfz1iso  10615  seq3coll  10616  seq3shft  10641  reval  10652  replim  10662  cj11  10708  caucvgre  10784  cvg1nlemcau  10787  cvg1nlemres  10788  rexuz3  10793  absval  10804  resqrexlemover  10813  resqrexlemdecn  10815  resqrexlemlo  10816  resqrexlemcalc3  10819  resqrexlemnm  10821  resqrexlemcvg  10822  resqrexlemoverl  10824  resqrexlemglsq  10825  resqrexlemga  10826  resqrexlemsqa  10827  resqrexlemex  10828  abs00bd  10869  cau3lem  10917  caubnd2  10920  climconst  11090  climmpt  11100  climshftlemg  11102  climcn1  11108  climle  11134  climub  11144  climserle  11145  climcau  11147  climcvg1nlem  11149  climcvg1n  11150  serf0  11152  fsum3cvg  11178  summodclem3  11180  summodclem2a  11181  summodclem2  11182  summodc  11183  zsumdc  11184  fsum3  11187  fsumf1o  11190  fisumss  11192  fsum3cvg2  11194  fsum3ser  11197  fsumcl2lem  11198  fsumadd  11206  sumsnf  11209  isummulc2  11226  isumge0  11230  isumadd  11231  fsum2dlemstep  11234  fsummulc2  11248  fsumconst  11254  fsumrelem  11271  isumshft  11290  isum1p  11292  isumnn0nn  11293  isumrpcl  11294  isumlessdc  11296  cvgratnnlemnexp  11324  cvgratnnlemmn  11325  cvgratnnlemseq  11326  cvgratnnlemabsle  11327  cvgratnnlemfm  11329  cvgratnnlemrate  11330  cvgratnn  11331  cvgratz  11332  mertenslemi1  11335  mertenslem2  11336  mertensabs  11337  clim2prod  11339  prodfap0  11345  prodfrecap  11346  prodfdivap  11347  fproddccvg  11372  prodmodclem3  11375  prodmodclem2a  11376  prodmodclem2  11377  prodmodc  11378  zproddc  11379  eftvalcn  11398  ef0lem  11401  ege2le3  11412  efcj  11414  efaddlem  11415  eftlub  11431  efgt1p2  11436  reef11  11440  tanvalap  11449  efieq1re  11512  eirraplem  11517  dvdsabseq  11579  dvdsfac  11592  zsupcllemex  11673  infssuzex  11676  gcd0id  11701  nn0seqcvgd  11756  alginv  11762  algcvg  11763  algcvga  11766  algfx  11767  eucalglt  11772  lcmid  11795  qredeu  11812  prmfac1  11864  sqne2sq  11889  qnumdenbi  11904  dfphi2  11930  ennnfonelemk  11947  ennnfonelemp1  11953  ennnfoneleminc  11958  ennnfonelemkh  11959  ennnfonelemhf1o  11960  ennnfonelemex  11961  ennnfonelemhom  11962  ennnfonelemrn  11966  ennnfonelemnn0  11969  ennnfonelemr  11970  ennnfonelemim  11971  ctinfomlemom  11974  ctinfom  11975  ctiunctlemfo  11986  sloteq  12001  topnvalg  12169  istps  12236  clsfval  12307  cnpval  12404  lmconst  12422  txcnp  12477  upxp  12478  uptx  12480  txlm  12485  lmcn2  12486  cnmpt11  12489  cnmpt11f  12490  cnmpt1t  12491  cnmpt21  12497  cnmpt21f  12498  cnmpt2t  12499  mopnval  12648  isxms  12657  isms  12659  comet  12705  mopnex  12711  xmetxp  12713  xmetxpbl  12714  txmetcnp  12724  txmetcn  12725  qtopbasss  12727  cncfi  12771  cncfmpt1f  12790  ivthinclemlm  12818  ivthinclemum  12819  ivthinclemlopn  12820  ivthinclemlr  12821  ivthinclemuopn  12822  ivthinclemur  12823  ivthinclemdisj  12824  ivthinclemloc  12825  ivthinc  12827  ivthdec  12828  cnlimci  12848  limccnpcntop  12850  eldvap  12857  dvcoapbr  12877  dvcj  12879  dvfre  12880  dvmptcjx  12892  dveflem  12893  sin0pilem2  12909  pilem3  12910  coseq0q4123  12961  coseq0negpitopi  12963  cos11  12980  logltb  13001  rpcxpef  13021  rplogbval  13068  012of  13361  2o01f  13362  subctctexmid  13367  nnsf  13372  nninfalllemn  13375  nninfalllem1  13376  nninfomnilem  13387  nninffeq  13389  qdencn  13395  trilpolemclim  13402  trilpolemcl  13403  trilpolemisumle  13404  trilpolemeq1  13406  trilpolemlt1  13407  trilpo  13409  redcwlpo  13420  dcapncf  13421  neapmkv  13423
  Copyright terms: Public domain W3C validator