Theorem fveq2 3800

Description: Equality theorem for function value.

Assertion

Ref	Expression
fveq2	|- (A = B -> (F` A) = (F` B))

Proof of Theorem fveq2

Step	Hyp	Ref	Expression
1		sneq 2462	. . . . . 6 |- (A = B -> {A} = {B})
2	1	imaeq2d 3467	. . . . 5 |- (A = B -> (F"{A}) = (F"{B}))
3	2	eqeq1d 1520	. . . 4 |- (A = B -> ((F"{A}) = {x} <-> (F"{B}) = {x}))
4	3	abbidv 1614	. . 3 |- (A = B -> {x | (F"{A}) = {x}} = {x | (F"{B}) = {x}})
5	4	unieqd 2560	. 2 |- (A = B -> U.{x | (F"{A}) = {x}} = U.{x | (F"{B}) = {x}})
6		df-fv 3253	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
7		df-fv 3253	. 2 |- (F` B) = U.{x | (F"{B}) = {x}}
8	5, 6, 7	3eqtr4g 1568	1 |- (A = B -> (F` A) = (F` B))

Syntax hints:   -> wi 3   = wceq 988  {cab 1499  {csn 2454  U.cuni 2551  "cima 3228  ` cfv 3237

This theorem is referenced by:  fveq2i 3803  fveq2d 3804  tz6.12-2 3815  funbrfv 3826  fnbrfvb 3829  dffn5 3834  ssimaex 3844  eqfnfvf 3874  elrnopabg 3876  fvelrn 3888  ffnfvf 3905  fnressn 3913  fressnfv 3914  fopabsn 3916  fvi 3918  fconstfv 3925  fvresex 3933  abrexexlem2 3935  funiunfv 3942  funiunfvf 3946  dff13f 3951  f1fveq 3952  f1ocnvfv 3956  f1ocnvfvb 3957  f1ocnvfv3 3959  isorel 3970  isocnv 3972  isotr 3973  isotrALT 3974  f1owe 3981  f1oweALT 3982  canth 3983  tfrlem1 3987  tfrlem2 3988  tfrlem11 3997  tfr2 4001  tfr3 4002  tz7.44-1 4004  tz7.44-2 4005  tz7.44-3 4006  rdglem1 4013  rdglem2 4014  rdgsuc 4021  rdglim 4024  tz7.48lem 4031  tz7.49 4035  abianfplem 4037  abianfp 4038  ffnoprval 4091  eqfnoprval 4093  fnoprval 4094  fnrnoprval 4114  fooprval 4115  oprvalex 4119  1stval2 4167  2ndval2 4168  1st2val 4175  2nd2val 4176  eqop 4181  unielxp 4184  sbcopeq1a 4188  csbopeq1a 4189  dfopab2 4190  dfoprab3 4191  dfoprab5s 4196  elrnoprabg 4204  1stconst 4206  2ndconst 4207  oav 4234  omv 4235  oev 4237  oev2 4246  omsmolem 4340  dom2d 4491  mapenlem2 4579  unblem2 4628  inf3lemd 4698  inf3lem1 4699  inf3lem2 4700  inf3lem5 4703  trcl 4731  r1tr 4740  r1ord 4741  r1ord3 4743  r1val1 4744  tz9.12lem3 4747  tz9.12 4748  rankvalg 4755  rankr1 4760  rankr1g 4761  ranklim 4771  r1pwcl 4773  ranksn 4775  rankonid 4781  rankeq0 4782  rankr1id 4783  rankuni 4784  rankxplim 4798  scottex 4802  scott0 4803  scottexs 4804  scott0s 4805  karden 4812  aceq3lem 4818  aceq4 4820  aceq5 4826  aceq6b 4828  ac6lem 4840  numthlem 4869  numth 4870  zorn2lem6 4879  unidom 4894  uniimadomf 4897  oncard 4916  carduni 4947  cardiun 4948  cardprc 4950  alephon 4954  alephcard 4956  alephordlem2 4962  alephordi 4963  alephord 4964  alephle 4973  cardaleph 4974  cardalephex 4975  alephfplem2 4986  alephfplem3 4987  alephfplem4 4988  alephfp2 4990  alephval2 4991  alephval3 4992  cf0 4999  cardcf 5000  cflecard 5001  cfeq0 5003  cfsuc 5004  reclem1pr 5245  reclem2pr 5246  reclem3pr 5247  monoord 6415  icoshftf1oii 6469  uz11 6492  fsequb 6583  om2uzsuci 6588  om2uzuzi 6589  om2uzlti 6590  om2uzlt2i 6591  seq1lem1 6602  seq1rval 6604  seq1val2 6607  seq1suclem 6609  seq1rn2 6614  seq1res 6620  ser1recli 6624  ser1monoi 6630  ser1add2i 6631  ser1addi 6632  seq1shftid 6649  seqzfval 6660  seqzfveq 6677  seqzrn2 6679  seqzres2 6684  ser0cl1i 6687  expval 6693  sqrthi 6822  sqrcli 6823  sqrgt0i 6824  sqrge0i 6825  sqr11i 6826  sqrmuli 6828  sqrcl 6833  sqrgt0 6834  sqrge0 6835  sqrle 6836  sqr00 6837  sqsqr 6846  absval 6885  cjval 6886  cjreb 6923  cjmulrcl 6924  cjmulval 6925  cjmulge0 6926  reneg 6927  readd 6928  imneg 6930  imadd 6931  cjcj 6934  cjadd 6935  cjmul 6936  cjneg 6937  addcj 6938  abs00i 6965  absval2 6975  abs00 6976  absge0 6977  absmul 6981  absdiv 6983  absid 6985  abslt 7003  absle 7004  abssubne0 7005  cjdiv 7012  absgt0 7016  abstri 7021  abs1mi 7027  abslem2 7032  seq1bndi 7033  seq1ublem 7034  cau2i 7036  caurei 7050  cauimi 7051  ser1absdiflem 7052  facp1 7059  faccl 7063  facdiv 7065  facwordi 7067  faclbnd 7068  faclbnd4lem1 7071  faclbnd4lem2 7072  faclbnd4lem3 7073  faclbnd4lem4 7074  bcval 7081  dffsum 7121  fsumserzfi 7123  ser1ser0i 7171  serzcl2 7172  serz1p 7175  serzmulci 7181  serzrelem 7184  clm4a 7213  clmi2a 7214  climconst3 7219  climshfti 7227  iserzshft2i 7230  serzclim0 7232  climrecl 7233  climge0 7235  climaddlem1 7237  climaddlem3 7239  climmullem6 7248  climmullem8 7250  climsub 7253  climcmplem 7260  climabslem 7271  climubii 7276  climubi 7277  climcaui 7279  caucvglem2 7281  caucvgi 7286  caucvg3i 7290  caucvg3 7291  serzf0i 7292  ser1f0i 7293  ser1consti 7294  ser1cmpi 7297  ser1cmp2i 7300  iserzabsi 7302  cvgcmp2lem 7303  cvgcmp2i 7304  cvgcmp2ci 7306  cvgcmp3cei 7310  cvgcmp3cetlem1 7311  cvgcmp3cetlem2 7312  isumvaltfi 7316  isum1p 7329  isumnn0nnai 7331  iserzgt0 7334  isummulc1 7335  isummulc1iALT 7336  isummulc1ai 7337  isumcmpii 7338  reccnv 7341  expcnv 7356  geoseri 7357  geolimi 7359  geolim 7360  geolim1 7362  geoisumr 7366  cvgratlem1ALT 7370  cvgratlem3ALT 7372  cvgratlem1 7373  cvgratlem3 7375  cvgratlem4 7376  negfcncfi 7392  ivthlem4 7407  ivthlem6 7409  ivthlem7 7410  ivthlem8 7411  ivthlem9 7412  dsupivthlem 7414  efcltlem1 7427  dfef2i 7430  ef0lem 7433  efcl 7435  efcvg 7437  eftval 7439  reefcl 7441  erelem3 7444  erelem6 7447  ege2lem2 7451  ege2le3lem2 7452  efcj 7460  efaddlem6 7466  efadd 7490  ef1tlubi 7505  ef01tllem1 7506  ef01tllem2 7507  ef01tllem2OLD 7508  ef01tlubi 7509  absef01tlubi 7511  ef4p 7524  efgt0i 7528  efgt0 7529  efltbi 7531  reef11 7533  eflegeo 7540  efm1legeo 7542  efcnlem4 7546  reeff1olem1 7548  reeff1o 7550  reefiso 7552  sinadd 7577  cosadd 7578  absef 7608  acdc3lem 7611  acdc3 7612  acdclem 7619  acdc 7620  acdcALT 7621  ruclem4 7638  ruclem25 7659  ruclem29 7663  ruclem33 7667  ruclem35 7669  ruclem37 7671  infmap2lem2 7705  clsfval 7788  0ntr 7822  lpfval 7862  cnpval 7879  metxpdval 7949  metxp 7954  opnfval 7977  methaus 8002  metcni 8014  iscau3 8058  iscau4 8060  iscaunns 8064  iscms 8066  lmfexlem2 8077  lmle 8080  metelcls 8085  metcnp4lem1 8088  metcnp4lem2 8089  metcnp4 8090  metcn4i 8092  xplmi 8093  xplm 8095  xpcn 8096  bopcnlem2 8102  fsumcnlem 8109  lmcau 8116  bcthlem2 8120  bcthlem10 8128  bcthlem15 8133  bcthlem16 8134  bcthlem17 8135  bcthlem18 8136  bcthlem20 8138  bcthlem28 8146  bcthlem29 8147  bcthlem33 8151  bcth 8152  grpinvfval 8185  grpinvf 8198  grpdivfval 8200  grpdivval 8201  ghgrpilem1 8252  nvvcop 8332  bafval 8342  isnvlem 8348  nvi 8352  nvs 8409  nvz 8416  nvtri 8417  imsval 8435  imsmet 8443  sqcn 8454  nmcn 8458  ipfval 8471  iporthcom 8488  ip1cnilem2 8493  sspval 8501  isssp 8502  lnoval 8532  lnolin 8534  nmofval 8544  nmosetn0 8547  nmolb 8553  nmoubi 8554  nmobndseqi 8559  isblo 8561  0ofval 8566  nmo0 8570  nmlno0lem 8572  nmlno0i 8573  nmlnoubi 8575  lnon0 8577  nmblolbii 8578  nmblolbi 8579  blocnilem 8583  ajfval 8588  phpar2 8601  phpar 8602  ipdir 8621  ipass 8624  sii 8633  isbn 8643  ubthlem1 8648  ubthlem3 8650  minveclem6 8669  minveclem7 8670  minveclem8 8671  minveclem23 8686  minveclem27 8690  minveclem33 8696  minveceu 8702  htthlem2 8740  htthlem3 8741  htthlem4 8742  sincolem 8783  pilem1 8789  pilem2 8790  pilem3 8791  pilem4 8792  cosh111lem2 8834  cosh111 8836  efif 8840  efifolem1 8841  efifolem2 8842  efifolem3 8843  efifolem6 8846  efifo 8848  efif1lem5 8853  efielcirc 8858  circgrp 8859  eff1i 8863  effoi 8864  pilog 8887  logltb 8895  orthcom 9094  normlem7tALT 9105  normsq 9121  norm-ii 9125  norm-iii 9127  normpyth 9132  normpar 9142  bcsiALT 9166  bcs 9168  hcau2 9175  hlimcauii 9226  norm1exi 9242  occllem3 9295  occllem5 9297  occl 9302  projlem22 9327  projlem23 9328  projlem26 9331  pjthlem8 9346  pjth 9354  pjtheu 9356  pjmval 9358  omlsi 9366  ococ 9368  axpjpj 9376  pjoc1 9387  pjoml 9389  pjoc2 9392  chocin 9538  chsscon3 9543  chjo 9558  chdmm1 9568  spanun 9588  hosval 9636  hosvalOLD 9637  homval 9638  hodval 9639  hodvalOLD 9640  hfsval 9641  hfmval 9642  cmbr 9647  pjoml6i 9652  cmbr3 9671  pjoml2 9674  pjoml3 9675  cmcm3 9678  osumlem8 9705  osum 9708  pjch1 9735  pjadji 9750  pjaddi 9751  pjinormi 9752  pjsubi 9753  pjmuli 9754  pjige0 9756  pjcjt2 9757  pjch 9759  pjjsi 9765  pjrni 9767  pjfo 9771  pj11i 9776  pj11 9779  pjopyth 9785  pjnorm 9789  pjpyth 9790  pjnel 9791  adjsym 9879  eigre 9881  elbdop 9905  nmopsetn0 9910  nmfnsetn0 9923  eigvalval 9941  nmoplb 9949  nmopub 9950  cnopc 9955  lnopl 9956  unop 9957  hmop 9964  nmfnlb 9966  nmfnleub 9967  elnlfn 9970  cnfnc 9972  lnfnl 9973  adj1 9975  eleigvec 9999  eigval1 10002  nmop0 10027  nmfn0 10028  nmlnop0iALT 10037  nmlnop0 10040  lnopeq0lem2 10048  lnopeq0i 10049  lnopunilem1 10052  lnopunii 10054  elunop2 10055  lnophmlem1 10058  lnophmi 10060  lnophm 10061  nmbdoplbi 10066  nmbdoplb 10067  nmcopexlem6 10073  nmcoplbi 10075  nmcopex 10076  nmcoplb 10077  nmophmi 10078  lnopconi 10080  nmbdfnlbi 10095  nmbdfnlb 10096  nmcfnexlem6 10102  nmcfnlbi 10104  nmcfnex 10105  nmcfnlb 10106  lnfnconi 10107  nlelchi 10111  riesz3i 10112  riesz1 10115  cnlnadjlem1 10117  cnlnadjlem5 10121  adjbd1o 10135  adjeq0 10141  branmfn 10155  rnbra 10157  pjbdlni 10193  pjhmop 10194  hmopidmchi 10196  hmopidmpji 10197  pjss2coi 10209  pjssmi 10210  pjssge0i 10211  pjdifnormi 10212  pjidmco 10226  pjhmopidm 10227  elpjrnch 10236  pjin2i 10239  pjclem1 10241  hstel2 10264  stge0 10269  stle1 10270  hst1h 10272  stj 10280  strlem1 10295  strlem2 10296  hstrlem2 10304  stcltr1i 10319  dmdmd 10345  atord 10433  irredi 10439  mdsymi 10456  cdj1i 10478  cdj3lem1 10479  cdj3lem2a 10481  cdj3lem2b 10482  cdj3lem3a 10484  cdj3lem3b 10485  cdj3i 10486  abs2sqlet 10495  abs2sqltt 10496  ghomgrpilem1 10506  ghomgrpilem2 10507  ghomsn 10509  ghomgrplem 10510  ghomlin 10514  ghomf1olem 10517  symggrp 10529  cayleylem2 10531  fveleq 10538  findreccl 10540  findabrcl 10541  sfvlim 10729  sfvlimOLD 10730  limfillem2OLD 10732  ist1 10738  iscon 10751  iscon2 10752  eloi 10794  1ded 10806  idosd 10812  cmppfd 10813  domcmpd 10814  codcmpd 10815  cmpasso 10841  cmpida 10842  cmpidb 10843  ishoma 10850  ishomc 10852  ishomd 10853  eqidob 10858  ismona 10872  ismonb 10873  ismonb2 10875  isepia 10882  isepib 10883  isepib2 10885  cinvlem1 10890  cinvlem2 10891  isfuna 10896  idfisf 10902

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-xp 3239  df-cnv 3241  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fv 3253

Copyright terms: Public domain