Theorem fveq2 3835

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 2475	. . . . . 6 |- (A = B -> {A} = {B})
2	1	imaeq2d 3496	. . . . 5 |- (A = B -> (F"{A}) = (F"{B}))
3	2	eqeq1d 1526	. . . 4 |- (A = B -> ((F"{A}) = {x} <-> (F"{B}) = {x}))
4	3	abbidv 1620	. . 3 |- (A = B -> {x | (F"{A}) = {x}} = {x | (F"{B}) = {x}})
5	4	unieqd 2578	. 2 |- (A = B -> U.{x | (F"{A}) = {x}} = U.{x | (F"{B}) = {x}})
6		df-fv 3279	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
7		df-fv 3279	. 2 |- (F` B) = U.{x | (F"{B}) = {x}}
8	5, 6, 7	3eqtr4g 1574	1 |- (A = B -> (F` A) = (F` B))

Syntax hints:   -> wi 3   = wceq 992  {cab 1505  {csn 2467  U.cuni 2569  "cima 3254  ` cfv 3263

This theorem is referenced by:  fveq2i 3838  fveq2d 3839  tz6.12-2 3850  funbrfv 3861  fnbrfvb 3864  dffn5 3869  ssimaex 3879  eqfnfvf2 3912  elrnopabg 3914  fvelrn 3926  ffnfvf 3943  fnressn 3951  fressnfv 3952  fopabsn 3954  fvi 3956  fconstfv 3963  fvresex 3971  abrexexlem2 3973  funiunfv 3980  funiunfvf 3984  dff13f 3989  f1fveq 3990  f1ocnvfv 3994  f1ocnvfvb 3995  f1ocnvfv3 3997  isorel 4008  isocnv 4010  isotr 4011  isotrALT 4012  f1owe 4019  f1oweALT 4020  ffnoprv 4074  eqfnoprv 4076  fnoprv 4077  fnrnoprv 4097  fooprv 4098  oprvex 4102  1stval2 4150  2ndval2 4151  1st2val 4158  2nd2val 4159  eqop 4164  unielxp 4167  sbcopeq1a 4171  csbopeq1a 4172  dfopab2 4173  dfoprab3 4174  dfoprab5s 4177  elrnoprabg 4186  df1st2 4188  df2nd2 4189  1stconst 4190  2ndconst 4191  fsplit 4204  canth 4205  onfununi 4209  tfrlem1 4212  tfrlem2 4213  tfrlem11 4222  tfr2 4226  tfr3 4227  tz7.44-1 4229  tz7.44-2 4230  tz7.44-3 4231  rdglem1 4238  rdglem2 4239  rdgsuc 4246  rdglim 4249  tz7.48lem 4256  tz7.49 4260  abianfplem 4262  abianfp 4263  oav 4286  omv 4287  oev 4289  oev2 4298  omsmolem 4396  dom2d 4545  ac6sfilem3 4590  mapenlem2 4637  unblem2 4687  inf3lemd 4757  inf3lem1 4758  inf3lem2 4759  inf3lem5 4762  trcl 4791  r1tr 4800  r1ord 4801  r1ord3 4803  r1val1 4804  tz9.12lem3 4807  tz9.12 4808  rankvalg 4815  rankr1 4820  rankr1g 4821  ranklim 4831  r1pwcl 4833  ranksn 4835  rankonid 4841  rankeq0 4842  rankr1id 4843  rankuni 4844  rankxplim 4858  scottex 4862  scott0 4863  scottexs 4864  scott0s 4865  karden 4872  aceq3lem 4878  aceq4 4880  aceq5 4886  aceq6b 4888  ac6lem 4900  numthlem 4929  numth 4930  zorn2lem6 4939  unidom 4954  uniimadomf 4957  oncard 4976  carduni 5008  cardiun 5009  cardprc 5011  alephon 5015  alephcard 5017  alephordlem2 5023  alephordi 5024  alephord 5025  alephle 5034  cardaleph 5035  cardalephex 5036  alephfplem2 5047  alephfplem3 5048  alephfplem4 5049  alephfp2 5051  alephval2 5052  alephval3 5053  cf0 5060  cardcf 5061  cflecard 5062  cfeq0 5064  cfsuc 5065  reclem1pr 5310  reclem2pr 5311  reclem3pr 5312  monoord 6482  icoshftf1oii 6536  uz11 6559  fsequb 6654  om2uzsuci 6659  om2uzuzi 6660  om2uzlti 6661  om2uzlt2i 6662  cardfz 6671  seq1lem1 6674  seq1rval 6676  seq1val2 6679  seq1suclem 6681  seq1rn2 6686  seq1res 6692  ser1recli 6696  ser1monoi 6702  ser1add2i 6703  ser1addi 6704  seq1shftid 6721  seqzfval 6732  seqzfveq 6749  seqzrn2 6751  seqzres2 6756  ser0cl1i 6759  expval 6765  sqrthi 6900  sqrcli 6901  sqrgt0i 6902  sqrge0i 6903  sqr11i 6904  sqrmuli 6906  sqrcl 6911  sqrgt0 6912  sqrge0 6913  sqrle 6914  sqr00 6915  sqsqr 6924  absval 6963  cjval 6964  cjreb 7001  cjmulrcl 7002  cjmulval 7003  cjmulge0 7004  reneg 7005  readd 7006  imneg 7008  imadd 7009  cjcj 7012  cjadd 7013  cjmul 7014  cjneg 7015  addcj 7016  cj11 7031  abs00i 7044  absval2 7054  abs00 7055  absge0 7056  absmul 7060  absdiv 7062  absid 7064  abslt 7083  absle 7084  abssubne0 7085  cjdiv 7092  absgt0 7096  abstri 7101  abs1mi 7107  abslem2 7112  seq1bndi 7113  seq1ublem 7114  cau2i 7116  caurei 7130  cauimi 7131  ser1absdiflem 7132  facp1 7139  faccl 7143  facdiv 7145  facwordi 7147  faclbnd 7148  faclbnd4lem1 7151  faclbnd4lem2 7152  faclbnd4lem3 7153  faclbnd4lem4 7154  bcval 7161  dffsum 7201  fsumserzfi 7203  ser1ser0i 7251  serzcl2 7252  serz1p 7255  serzmulci 7261  serzrelem 7264  clm4a 7293  clmi2a 7294  climconst3 7299  climshfti 7307  iserzshft2i 7310  serzclim0 7312  climrecl 7313  climge0 7315  climaddlem1 7317  climaddlem3 7319  climmullem6 7328  climmullem8 7330  climsub 7333  climcmplem 7340  climabslem 7351  climubii 7356  climubi 7357  climcaui 7359  caucvglem2 7361  caucvgi 7366  caucvg3i 7370  caucvg3 7371  serzf0i 7372  ser1consti 7374  ser1cmpi 7377  ser1cmp2i 7380  iserzabsi 7382  cvgcmp2lem 7383  cvgcmp2i 7384  cvgcmp2ci 7387  cvgcmp3cei 7391  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  isumvaltfi 7397  isum1p 7410  isumnn0nnai 7412  iserzgt0 7415  isummulc1 7416  isummulc1iALT 7417  isummulc1ai 7418  isumcmpii 7419  reccnv 7422  expcnv 7437  explecnv 7438  geoseri 7439  geolimi 7441  geolim 7442  geolim1 7444  geoisumr 7448  cvgratlem1ALT 7452  cvgratlem3ALT 7454  cvgratlem1 7455  cvgratlem3 7457  cvgratlem4 7458  negfcncfi 7474  ivthlem4 7489  ivthlem6 7491  ivthlem7 7492  ivthlem8 7493  ivthlem9 7494  dsupivthlem 7496  efcltlem1 7509  dfef2i 7512  ef0lem 7515  efcl 7517  efcvg 7519  eftval 7521  reefcl 7523  erelem3 7526  erelem6 7529  ege2lem2 7533  ege2le3lem2 7534  efcj 7542  efaddlem6 7548  efadd 7572  ef1tlubi 7587  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  ef01tlubi 7591  absef01tlubi 7593  ef4p 7608  efgt0i 7612  efgt0 7613  efltbi 7615  reef11 7617  eflegeo 7624  efm1legeo 7626  efcnlem4 7630  reeff1olem1 7632  reeff1o 7634  reefiso 7636  sinadd 7661  cosadd 7662  absef 7692  efieq1re 7694  acdc3lem 7697  acdc3 7698  acdclem 7706  acdc 7707  acdcALT 7708  ruclem4 7725  ruclem25 7746  ruclem29 7750  ruclem33 7754  ruclem35 7756  ruclem37 7758  infmap2lem2 7792  clsfval 7878  0ntr 7912  lpfval 7952  cnpval 7969  metxpdval 8039  metxp 8044  opnfval 8067  methaus 8093  metcni 8105  iscau3 8149  iscau4 8151  iscaunns 8155  iscms 8157  lmfexlem2 8168  lmle 8171  metelcls 8176  metcnp4lem1 8179  metcnp4lem2 8180  metcnp4 8181  metcn4i 8183  xplmi 8184  xplm 8186  xpcn 8187  bopcnlem2 8193  fsumcnlem 8200  lmcau 8207  bcthlem2 8211  bcthlem10 8219  bcthlem15 8224  bcthlem16 8225  bcthlem17 8226  bcthlem18 8227  bcthlem20 8229  bcthlem28 8237  bcthlem29 8238  bcthlem33 8242  bcth 8243  grpidval 8275  grpinvfval 8283  grpinvf 8297  grpdivfval 8299  grpdivval 8300  gxoprval 8313  gxval 8314  gxcom 8325  gxid 8329  ghgrpilem1 8374  nvvcop 8460  bafval 8470  isnvlem 8476  nvi 8480  nvs 8537  nvz 8544  nvtri 8545  imsval 8563  imsmet 8571  vacnlem1 8582  vacnlem3 8584  vacnlem4 8585  vacnlem5 8586  vacnlem6 8587  vacn 8588  sqcn 8589  nmcn 8593  ipfval 8606  iporthcom 8623  ip1cnilem2 8628  sspval 8636  isssp 8637  lnoval 8667  lnolin 8669  nmofval 8679  nmosetn0 8682  nmolb 8688  nmoubi 8689  nmounbseqi 8694  nmobndseqi 8695  isblo 8697  0ofval 8702  nmo0 8706  nmlno0lem 8708  nmlno0i 8709  nmlnoubi 8711  lnon0 8713  nmblolbii 8714  nmblolbi 8715  blocnilem 8719  ajfval 8724  ishmo 8726  phpar2 8738  phpar 8739  ipdir 8758  ipass 8761  sii 8770  isbn 8781  ubthlem1 8787  ubthlem3 8789  minveclem6 8810  minveclem7 8811  minveclem8 8812  minveclem23 8827  minveclem27 8831  minveclem33 8837  minveceu 8843  htthlem2 8883  htthlem3 8884  htthlem4 8885  sincolem 8932  pilem1 8938  pilem2 8939  pilem3 8940  pilem4 8941  sineq0re 8985  cosh111lem2 8987  cosh111 8989  efif 8993  efifolem1 8994  efifolem2 8995  efifolem3 8996  efifolem6 8999  efifo 9001  efif1lem5 9006  efielcirc 9011  circgrp 9012  eff1i 9016  effoi 9017  pilog 9040  logltb 9048  orthcom 9250  normlem7tALT 9261  normsq 9277  norm-ii 9281  norm-iii 9283  normpyth 9288  normpar 9298  bcsiALT 9322  bcs 9324  hcau2 9331  hlimcauii 9382  norm1exi 9398  occllem3 9451  occllem5 9453  occl 9458  projlem22 9483  projlem23 9484  projlem26 9487  pjthlem8 9502  pjth 9510  pjtheu 9512  pjmval 9514  omlsi 9522  ococ 9524  axpjpj 9532  pjoc1 9543  pjoml 9545  pjoc2 9548  chocin 9694  chsscon3 9699  chjo 9714  chdmm1 9724  spanun 9744  hosval 9792  hosvalOLD 9793  homval 9794  hodval 9795  hodvalOLD 9796  hfsval 9797  hfmval 9798  cmbr 9803  pjoml6i 9808  cmbr3 9827  pjoml2 9830  pjoml3 9831  cmcm3 9834  osumlem8 9863  osum 9866  pjch1 9893  pjadji 9908  pjaddi 9909  pjinormi 9910  pjsubi 9911  pjmuli 9912  pjige0 9914  pjcjt2 9915  pjch 9917  pjjsi 9923  pjrni 9925  pjfo 9929  pj11i 9934  pj11 9937  pjopyth 9943  pjnorm 9947  pjpyth 9948  pjnel 9949  adjsym 10039  eigre 10041  eigorth 10044  elbdop 10067  nmopsetn0 10072  nmfnsetn0 10085  eigvalval 10103  nmoplb 10111  nmopub 10112  cnopc 10117  lnopl 10118  unop 10119  hmop 10126  nmfnlb 10128  nmfnleub 10129  elnlfn 10132  cnfnc 10134  lnfnl 10135  adj1 10137  eleigvec 10161  eigval1 10164  nmop0 10189  nmfn0 10190  nmlnop0iALT 10199  nmlnop0 10202  lnopeq0lem2 10210  lnopeq0i 10211  lnopunilem1 10214  lnopunii 10216  elunop2 10217  lnophmlem1 10220  lnophmi 10222  lnophm 10223  nmbdoplbi 10228  nmbdoplb 10229  nmcopexlem6 10235  nmcoplbi 10237  nmcopex 10238  nmcoplb 10239  nmophmi 10240  lnopconi 10242  nmbdfnlbi 10257  nmbdfnlb 10258  nmcfnexlem6 10264  nmcfnlbi 10266  nmcfnex 10267  nmcfnlb 10268  lnfnconi 10269  nlelchi 10273  riesz3i 10274  riesz1 10277  cnlnadjlem1 10279  cnlnadjlem5 10283  adjbd1o 10297  adjeq0 10303  branmfn 10317  branmfnOLD 10318  rnbra 10320  pjbdlni 10356  pjhmop 10357  hmopidmchi 10359  hmopidmpji 10360  pjss2coi 10372  pjssmi 10373  pjssge0i 10374  pjdifnormi 10375  pjidmco 10389  pjhmopidm 10390  elpjrnch 10399  pjin2i 10402  pjclem1 10404  hstel2 10427  stge0 10432  stle1 10433  hst1h 10435  stj 10443  strlem1 10458  strlem2 10459  hstrlem2 10467  stcltr1i 10482  dmdmd 10508  atord 10597  irredi 10603  mdsymi 10620  cdj1i 10642  cdj3lem1 10643  cdj3lem2a 10645  cdj3lem2b 10646  cdj3lem3a 10648  cdj3lem3b 10649  cdj3i 10650  abs2sqlet 10659  abs2sqltt 10660  ghomgrpilem1 10670  ghomgrpilem2 10671  ghomsn 10673  ghomgrplem 10674  ghomlin 10678  ghomf1olem 10681  symggrp 10693  cayleylem2 10695  fveleq 10700  findreccl 10702  findabrcl 10703  eloi 10817  expus 10938  on1el3 10962  on1el4 10963  isdivrng 10968  nsn 11017  osneisi 11018  sfvlim 11100  limfillem2 11102  ist1 11106  iscon 11126  iscon2 11127  clsingemp 11130  1ded 11192  idosd 11198  cmppfd 11199  domcmpd 11200  codcmpd 11201  cmpasso 11227  cmpida 11228  cmpidb 11229  ishoma 11242  ishomc 11244  ishomd 11245  eqidob 11250  ismona 11264  ismonb 11265  ismonb2 11267  isepia 11274  isepib 11275  isepib2 11277  cinvlem1 11282  cinvlem2 11283  isfuna 11288  idfisf 11295  issubcat 11299  issubcata 11300  issubcatb 11301  idsubfun 11312  fictblem 11422  fictb 11423  ordiso 11426  ordtypelem5 11431  ordtypelem7 11433  hartoglem 11435  omsubsdomlem2 11441  omsubsdom 11442  omsubdom 11443  omsubel 11444  elomsubsd 11446  omsublim 11448  omsubindss 11449  infenomsub 11450  omsubinit 11451  fibas 11452  cldbnd 11462  opnregcld 11467  cldregopn 11468  cncls 11473  cnntr 11474  compsub 11488  hscptsscld 11491  alexsublem1 11496  alexsublem3 11498  alexsub 11500  ivthALT 11515  2ndcsb 11537  2ndcctbss 11539  islocfin 11567  comppfsc 11578  neibastop2lem1 11580  neibastop2lem3 11582  neibastop2lem4 11583  neibastop3 11585  isreg 11609  isnrm 11612  fsubbas 11630  fgf 11632  flimcls 11684  hausfillim 11685  cnpfillim 11686  flimff 11707  sflimf 11708  sfcls 11716  filclus 11717  isfclus 11718  fclsfnflim 11726  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomp 11733  ufcomp 11734  fclusff 11735  sfclusf 11736  filnetlem5 11767  filnet 11768  isgalem 11771  xp1st 11796  xp2nd 11797  oprabopabf 11807  oprabco 11811  f1elima 11818  cbvixpv 11821  upxp 11822  upixp 11823  findcard 11836  eluzadd 11860  eluzsub 11861  sdclem1 11875  sdclem2 11876  sdc 11877  seqpo 11878  incsequz 11879  incsequz2 11880  fsumltisum 11887  fsumleisumi 11889  fsumleisum 11890  isumclf 11891  iserzshft2 11892  isumshft2 11893  metf1o 11907  mettrifi 11912  mettrifi2 11913  geomcau 11914  lmclim2 11915  caushft 11916  tlmval 11964  haustlmu 11967  tlmconst 11968  uptx 11978  txcnopab 11980  txcnoprab 11981  2txcn 11982  istotbnd 11989  isbnd 11995  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem2 12012  heiborlem3 12013  heiborlem10 12020  heiborlem13 12023  heiborlem16 12026  heiborlem18 12028  heiborlem24 12034  heiborlem25 12035  heiborlem26 12036  heiborlem29 12039  heiborlem30 12040  heiborlem31 12041  heiborlem32 12042  heiborlem33 12043  heiborlem35 12045  heiborlem36 12046  heiborlem42 12052  bfplem3 12056  bfplem5 12058  bfplem6 12059  bfplem8 12061  bfplem9 12062  bfplem10 12063  bfplem11 12064  rrnmet 12072  rrndstprj 12073  rrndstprj2 12074  rrncms 12075  rrntotbndlem2 12077  ismrer1 12080  phtpyid 12091  phtpycom 12092  phtpycolem3 12095  phtpycolem4 12096  phtpycolem5 12097  phtpyco 12098  phtpcval 12100

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279

Copyright terms: Public domain