Theorem fveq2 3715

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 2413	. . . . . 6 |- (A = B -> {A} = {B})
2	1	imaeq2d 3396	. . . . 5 |- (A = B -> (F"{A}) = (F"{B}))
3	2	eqeq1d 1480	. . . 4 |- (A = B -> ((F"{A}) = {x} <-> (F"{B}) = {x}))
4	3	abbidv 1574	. . 3 |- (A = B -> {x | (F"{A}) = {x}} = {x | (F"{B}) = {x}})
5	4	unieqd 2507	. 2 |- (A = B -> U.{x | (F"{A}) = {x}} = U.{x | (F"{B}) = {x}})
6		df-fv 3193	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
7		df-fv 3193	. 2 |- (F` B) = U.{x | (F"{B}) = {x}}
8	5, 6, 7	3eqtr4g 1528	1 |- (A = B -> (F` A) = (F` B))

Syntax hints:   -> wi 3   = wceq 954  {cab 1461  {csn 2405  U.cuni 2498  "cima 3168  ` cfv 3177

This theorem is referenced by:  fveq2i 3718  fveq2d 3719  tz6.12-2 3730  funbrfv 3741  fnbrfvb 3744  fnopabfv 3749  ssimaex 3759  eqfnfvf 3789  elrnopabg 3791  fvelrn 3803  ffnfvf 3820  fnressn 3828  fressnfv 3829  fopabsn 3831  fvi 3833  fconstfv 3840  fvresex 3848  abrexexlem2 3850  funiunfv 3857  funiunfvf 3861  f1fvf 3866  f1fveq 3867  f1ocnvfv 3871  f1ocnvfvb 3872  f1ocnvfv3 3874  isorel 3885  isocnv 3887  isotr 3888  isotrALT 3889  f1owe 3896  f1oweALT 3897  canth 3898  tfrlem1 3902  tfrlem2 3903  tfrlem11 3912  tfr2 3916  tfr3 3917  tz7.44-1 3919  tz7.44-2 3920  tz7.44-3 3921  rdglem1 3928  rdglem2 3929  rdgsuct 3936  rdglimt 3939  tz7.48lem 3946  tz7.49 3950  abianfplem 3952  abianfp 3953  ffnoprval 4005  eqfnoprval 4007  fnoprval 4008  fnrnoprval 4027  fooprval 4028  oprvalex 4032  1stval2 4079  2ndval2 4080  1st2val 4085  2nd2val 4086  2ndconst 4087  eqop 4094  unielxp 4097  sbcopeq1a 4101  csbopeq1a 4102  dfopab2 4103  dfoprab3 4104  dfoprab4 4106  elrnoprabg 4114  df1st2 4116  df2nd2 4117  oav 4140  omv 4141  oev 4143  oev2 4152  omsmolem 4246  dom2d 4391  mapenlem2 4476  unblem2 4524  inf3lemd 4592  inf3lem1 4593  inf3lem2 4594  inf3lem5 4597  trcl 4625  r1tr 4634  r1ord 4635  r1ord3 4637  r1val1 4638  tz9.12lem3 4641  tz9.12 4642  rankvalg 4649  rankr1 4654  rankr1g 4655  ranklim 4665  r1pwcl 4667  ranksn 4669  rankonid 4675  rankeq0 4676  rankr1id 4677  rankuni 4678  rankxplim 4692  scottex 4696  scott0 4697  scottexs 4698  scott0s 4699  karden 4706  aceq3lem 4712  aceq4 4714  aceq5 4720  aceq6b 4722  ac6lem 4734  numthlem 4763  numth 4764  zorn2lem6 4773  unidom 4788  uniimadomf 4791  oncard 4809  carduni 4838  cardiun 4839  cardprc 4841  alephon 4845  alephcard 4847  alephordlem2 4853  alephordi 4854  alephord 4855  alephle 4864  cardaleph 4865  cardalephex 4866  alephfplem2 4877  alephfplem3 4878  alephfplem4 4879  alephfp2 4881  alephval2 4882  alephval3 4883  cf0 4890  cardcf 4891  cflecard 4892  cfeq0 4894  cfsuc 4895  reclem1pr 5136  reclem2pr 5137  reclem3pr 5138  monoord 6239  om2uzsuc 6241  om2uzuz 6242  om2uzlt 6243  om2uzlt2 6244  seq1lem1 6254  seq1rval 6256  seq1val2 6259  seq1suclem 6261  seq1rn2 6266  seq1res 6272  ser1recl 6276  ser1mono 6282  ser1add2 6283  ser1add 6284  seq1shftid 6301  icoshftf1oi 6350  uz11t 6372  fsequb 6463  seqzfval 6477  seqzfveq 6494  seqzrn2 6496  seqzres2 6501  ser0cl1 6504  expvalt 6510  sqrth 6637  sqrcl 6638  sqrgt0 6639  sqrge0 6640  sqr11 6641  sqrmul 6643  sqrclt 6648  sqrgt0t 6649  sqrge0t 6650  sqrlet 6651  sqr00t 6652  sqsqrt 6661  absvalt 6702  cjvalt 6703  cjrebt 6743  cjmulrclt 6744  cjmulvalt 6745  cjmulge0t 6746  renegt 6747  readdt 6748  imnegt 6750  imaddt 6751  cjcjt 6754  cjaddt 6755  cjmult 6756  cjnegt 6757  addcjt 6758  abs00 6785  absval2t 6795  abs00t 6796  absge0t 6797  absmult 6801  absdivt 6803  absidt 6805  absltt 6825  abslttOLD 6826  abslet 6827  abssubne0t 6828  cjdivt 6835  absgt0t 6839  abstrit 6843  abs1m 6849  abslem2 6854  seq1bnd 6855  seq1ublem 6856  cau2 6858  caure 6872  cauim 6873  ser1absdiflem 6874  facp1t 6881  facclt 6885  facdivt 6887  facwordit 6889  faclbnd 6890  faclbnd4lem1 6893  faclbnd4lem2 6894  faclbnd4lem3 6895  faclbnd4lem4 6896  bcvalt 6903  dffsum 6944  fsumserzf 6946  ser1ser0 6994  serzcl2t 6995  serz1p 6998  serzmulc 7004  serzrelem 7007  clm4at 7036  clmi2at 7037  climconst3 7041  climshft 7049  iserzshft2 7052  serzclim0 7054  climrecl 7055  climge0 7057  climaddlem1 7058  climaddlem3 7060  climmullem6 7069  climmullem8 7071  climsub 7074  climcmplem 7081  climabslem 7092  climubi 7097  climub 7098  climcau 7100  caucvglem2 7102  caucvg 7107  caucvg3 7111  caucvg3t 7112  serzf0 7113  ser1f0 7114  ser1const 7115  ser1cmp 7118  ser1cmp2 7121  iserzabs 7123  cvgcmp2lem 7124  cvgcmp2 7125  cvgcmp2c 7127  cvgcmp3ce 7131  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  isumvaltf 7137  isum1p 7149  isumnn0nna 7151  iserzgt0 7154  isummulc1 7155  isummulc1ALT 7156  isummulc1a 7157  isumcmpi 7158  reccnv 7161  expcnv 7176  geoser 7177  geolimi 7179  geolim 7180  geolim1 7182  geoisumr 7186  cvgratlem1ALT 7190  cvgratlem3ALT 7192  cvgratlem1 7193  cvgratlem3 7195  cvgratlem4 7196  negfcncf 7212  ivthlem4 7227  ivthlem6 7229  ivthlem7 7230  ivthlem8 7231  ivthlem9 7232  dsupivthlem 7234  ivthlem4OLD 7236  ivthlem6OLD 7238  ivthlem7OLD 7239  ivthlem8OLD 7240  efcltlem1 7254  dfef2 7257  ef0lem 7260  efclt 7262  efcvg 7264  eftval 7266  reefclt 7268  erelem3 7271  erelem6 7274  ege2lem2 7278  ege2le3lem2 7279  efcjt 7287  efaddlem6 7293  efaddt 7317  ef1tlub 7332  ef01tllem1 7333  ef01tllem2 7334  ef01tlub 7335  absef01tlub 7337  ef4pt 7349  efgt0 7353  efgt0t 7354  efltb 7356  reeff1 7358  eflegeot 7364  efm1legeot 7366  efcnlem4 7370  reeff1olem1 7372  reeff1olem1OLD 7374  reeff1o 7376  reefiso 7378  sinaddt 7403  cosaddt 7404  abseft 7433  acdc3lem 7436  acdc3 7437  acdclem 7444  acdc 7445  acdcALT 7446  ruclem4 7464  ruclem25 7485  ruclem29 7489  ruclem33 7493  ruclem35 7495  ruclem37 7497  infmap2lem2 7530  clsfval 7618  0ntr 7652  lpfval 7692  cnpval 7709  metxpdval 7781  metxp 7786  opnfval 7809  methaus 7834  metcni 7846  iscau3 7890  iscau4 7892  iscms 7897  lmfexlem2 7908  lmle 7911  metelcls 7916  metcnp4lem1 7918  metcnp4lem2 7919  metcnp4 7920  metcn4i 7922  xplmi 7923  xplm 7925  xpcn 7926  bopcnlem2 7932  fsumcnlem 7939  lmcau 7946  bcthlem2 7950  bcthlem10 7958  bcthlem15 7963  bcthlem16 7964  bcthlem17 7965  bcthlem18 7966  bcthlem20 7968  bcthlem28 7976  bcthlem29 7977  bcthlem33 7981  bcth 7982  grpinvfval 8016  grpinvf 8029  grpdivfval 8031  grpdivval 8032  ghgrpilem1 8085  nvvcop 8165  bafval 8175  isnvlem 8181  nvi 8185  nvs 8242  nvz 8249  nvtri 8250  imsval 8267  imsmet 8275  sqcn 8283  nmcn 8287  ipfval 8299  iporthcom 8316  ip1cnilem2 8321  sspval 8329  isssp 8330  lnoval 8360  lnolin 8362  nmofval 8370  nmosetn0 8373  nmolb 8379  nmoubi 8380  nmobndseqi 8385  isblo 8387  0ofval 8392  nmo0 8396  nmlno0lem 8398  nmlno0i 8399  nmlnoubi 8401  nmblolbii 8403  nmblolbi 8404  blocnilem 8408  ajfval 8413  phpar2 8426  phpar 8427  ipdir 8446  ipass 8449  sii 8458  isbn 8468  ubthlem1 8473  ubthlem3 8475  minveclem6 8494  minveclem7 8495  minveclem8 8496  minveclem23 8511  minveclem27 8515  minveclem33 8521  minveceu 8527  htthlem2 8564  htthlem3 8565  htthlem4 8566  sincolem 8603  pilem1 8609  pilem2 8610  pilem3 8611  pilem4 8612  cosh111lem2 8649  cosh111t 8651  efif 8655  efifolem1 8656  efifolem2 8657  efifolem3 8658  efifolem6 8661  efifo 8663  efif1lem5 8668  elcircOLD 8673  efielcirc 8678  circgrp 8679  eff1i 8683  effoi 8684  pilog 8707  logltbt 8715  orthcom 8913  normlem7tALT 8924  normsqt 8940  norm-iit 8944  norm-iiit 8946  normpytht 8951  normpart 8961  bcsALT 8985  bcst 8987  hcau2 8994  hlimcaui 9045  norm1ex 9061  occllem3 9114  occllem5 9116  occlt 9121  projlem22 9146  projlem23 9147  projlem26 9150  pjthlem8 9164  pjtht 9172  pjtheut 9174  pjmvalt 9176  omls 9184  ococt 9186  axpjpjt 9194  pjoc1t 9205  pjomlt 9207  pjoc2t 9210  chocint 9356  chsscon3t 9361  chjot 9376  chdmm1t 9386  spanunt 9406  hosvalt 9456  hosvaltOLD 9457  homvalt 9458  hodvalt 9459  hodvaltOLD 9460  hfsvalt 9461  hfmvalt 9462  cmbrt 9467  pjoml6 9472  cmbr3t 9491  pjoml2t 9494  pjoml3t 9495  cmcm3t 9498  osumlem8 9525  osumt 9528  pjch1t 9555  pjadjt 9570  pjaddt 9571  pjinormt 9572  pjsubt 9573  pjmult 9574  pjige0t 9576  pjcjt2 9577  pjcht 9579  pjjs 9585  pjrn 9587  pjfot 9591  pj11 9596  pj11t 9599  pjopytht 9605  pjnormt 9609  pjpytht 9610  pjnelt 9611  adjsymt 9699  eigret 9701  eigortht 9704  elbdopt 9727  nmopsetn0 9732  nmfnsetn0 9745  eigvalvalt 9763  nmoplbt 9771  nmopubt 9772  cnopct 9776  lnoplt 9777  unopt 9778  hmopt 9785  nmfnlbt 9787  nmfnleubt 9788  elnlfnt 9791  cnfnct 9793  lnfnlt 9794  adjt 9796  eleigvect 9820  eigvalt 9823  nmop0 9849  nmfn0 9850  nmlnop0ALT 9858  nmlnop0t 9861  lnopeq0lem2 9869  lnopeq0 9870  lnopunilem1 9873  lnopuni 9875  elunop2t 9876  lnophmlem1 9879  lnophm 9881  lnophmt 9882  nmbdoplb 9887  nmbdoplbt 9888  nmcopexlem6 9894  nmcoplb 9896  nmcopext 9897  nmcoplbt 9898  nmophm 9899  lnopcon 9901  nmbdfnlb 9916  nmbdfnlbt 9917  nmcfnexlem6 9923  nmcfnlb 9925  nmcfnext 9926  nmcfnlbt 9927  lnfncon 9928  nlelch 9932  riesz3 9933  riesz1t 9936  cnlnadjlem1 9938  cnlnadjlem5 9942  adjbd1o 9956  adjeq0 9962  branmfnt 9976  rnbra 9978  pjbdln 10014  pjhmopt 10015  hmopidmch 10017  hmopidmpj 10018  pjss2co 10030  pjssmt 10031  pjssge0t 10032  pjdifnormt 10033  pjidmcot 10047  pjhmopidm 10048  elpjrncht 10056  pjin2 10059  pjclem1 10061  hstel2t 10084  stge0t 10089  stle1t 10090  hst1ht 10092  stjt 10100  strlem1 10115  strlem2 10116  hstrlem2 10124  stcltr1 10139  dmdmdt 10165  atordt 10252  irred 10258  mdsym 10275  cdj1 10294  cdj3lem1 10295  cdj3lem2a 10297  cdj3lem2b 10298  cdj3lem3a 10300  cdj3lem3b 10301  cdj3 10302  abs2sqlet 10308  abs2sqltt 10309  ghomgrpilem1 10319  ghomgrpilem2 10320  ghomsn 10322  ghomgrplem 10323  ghomlin 10327  ghomf1olem 10330  symggrp 10342  cayleylem2 10344  fveleq 10349  findreccl 10351  findabrcl 10352  ist1 10494  eloi 10539  1ded 10551  idosd 10557  cmppfd 10558  domcmpd 10559  codcmpd 10560  cmpasso 10586  cmpida 10587  cmpidb 10588  ishoma 10595  ishomc 10597  ishomd 10598  eqidob 10603  ismona 10615  ismonb 10616  ismonb2 10618  isfuna 10628

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193

Copyright terms: Public domain