Theorem fveq2 3724

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 2417	. . . . . 6 |- (A = B -> {A} = {B})
2	1	imaeq2d 3404	. . . . 5 |- (A = B -> (F"{A}) = (F"{B}))
3	2	eqeq1d 1483	. . . 4 |- (A = B -> ((F"{A}) = {x} <-> (F"{B}) = {x}))
4	3	abbidv 1577	. . 3 |- (A = B -> {x | (F"{A}) = {x}} = {x | (F"{B}) = {x}})
5	4	unieqd 2512	. 2 |- (A = B -> U.{x | (F"{A}) = {x}} = U.{x | (F"{B}) = {x}})
6		df-fv 3198	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
7		df-fv 3198	. 2 |- (F` B) = U.{x | (F"{B}) = {x}}
8	5, 6, 7	3eqtr4g 1531	1 |- (A = B -> (F` A) = (F` B))

Syntax hints:   -> wi 3   = wceq 956  {cab 1463  {csn 2409  U.cuni 2503  "cima 3173  ` cfv 3182

This theorem is referenced by:  fveq2i 3727  fveq2d 3728  tz6.12-2 3739  funbrfv 3750  fnbrfvb 3753  fnopabfv 3758  ssimaex 3768  eqfnfvf 3798  elrnopabg 3800  fvelrn 3812  ffnfvf 3829  fnressn 3837  fressnfv 3838  fopabsn 3840  fvi 3842  fconstfv 3849  fvresex 3857  abrexexlem2 3859  funiunfv 3866  funiunfvf 3870  f1fvf 3875  f1fveq 3876  f1ocnvfv 3880  f1ocnvfvb 3881  f1ocnvfv3 3883  isorel 3894  isocnv 3896  isotr 3897  isotrALT 3898  f1owe 3905  f1oweALT 3906  canth 3907  tfrlem1 3911  tfrlem2 3912  tfrlem11 3921  tfr2 3925  tfr3 3926  tz7.44-1 3928  tz7.44-2 3929  tz7.44-3 3930  rdglem1 3937  rdglem2 3938  rdgsuct 3945  rdglimt 3948  tz7.48lem 3955  tz7.49 3959  abianfplem 3961  abianfp 3962  ffnoprval 4014  eqfnoprval 4016  fnoprval 4017  fnrnoprval 4036  fooprval 4037  oprvalex 4041  1stval2 4089  2ndval2 4090  1st2val 4095  2nd2val 4096  2ndconst 4097  eqop 4104  unielxp 4107  sbcopeq1a 4111  csbopeq1a 4112  dfopab2 4113  dfoprab3 4114  dfoprab4 4116  elrnoprabg 4124  df1st2 4126  df2nd2 4127  oav 4150  omv 4151  oev 4153  oev2 4162  omsmolem 4256  dom2d 4404  mapenlem2 4490  unblem2 4541  inf3lemd 4612  inf3lem1 4613  inf3lem2 4614  inf3lem5 4617  trcl 4645  r1tr 4654  r1ord 4655  r1ord3 4657  r1val1 4658  tz9.12lem3 4661  tz9.12 4662  rankvalg 4669  rankr1 4674  rankr1g 4675  ranklim 4685  r1pwcl 4687  ranksn 4689  rankonid 4695  rankeq0 4696  rankr1id 4697  rankuni 4698  rankxplim 4712  scottex 4716  scott0 4717  scottexs 4718  scott0s 4719  karden 4726  aceq3lem 4732  aceq4 4734  aceq5 4740  aceq6b 4742  ac6lem 4754  numthlem 4783  numth 4784  zorn2lem6 4793  unidom 4808  uniimadomf 4811  oncard 4829  carduni 4858  cardiun 4859  cardprc 4861  alephon 4865  alephcard 4867  alephordlem2 4873  alephordi 4874  alephord 4875  alephle 4884  cardaleph 4885  cardalephex 4886  alephfplem2 4897  alephfplem3 4898  alephfplem4 4899  alephfp2 4901  alephval2 4902  alephval3 4903  cf0 4910  cardcf 4911  cflecard 4912  cfeq0 4914  cfsuc 4915  reclem1pr 5156  reclem2pr 5157  reclem3pr 5158  monoord 6294  om2uzsuc 6296  om2uzuz 6297  om2uzlt 6298  om2uzlt2 6299  seq1lem1 6309  seq1rval 6311  seq1val2 6314  seq1suclem 6316  seq1rn2 6321  seq1res 6327  ser1recl 6331  ser1mono 6337  ser1add2 6338  ser1add 6339  seq1shftid 6356  icoshftf1oi 6409  uz11t 6432  fsequb 6523  seqzfval 6537  seqzfveq 6554  seqzrn2 6556  seqzres2 6561  ser0cl1 6564  expvalt 6570  sqrth 6699  sqrcl 6700  sqrgt0 6701  sqrge0 6702  sqr11 6703  sqrmul 6705  sqrclt 6710  sqrgt0t 6711  sqrge0t 6712  sqrlet 6713  sqr00t 6714  sqsqrt 6723  absvalt 6762  cjvalt 6763  cjrebt 6800  cjmulrclt 6801  cjmulvalt 6802  cjmulge0t 6803  renegt 6804  readdt 6805  imnegt 6807  imaddt 6808  cjcjt 6811  cjaddt 6812  cjmult 6813  cjnegt 6814  addcjt 6815  abs00 6842  absval2t 6852  abs00t 6853  absge0t 6854  absmult 6858  absdivt 6860  absidt 6862  absltt 6880  abslet 6881  abssubne0t 6882  cjdivt 6889  absgt0t 6893  abstrit 6898  abs1m 6904  abslem2 6909  seq1bnd 6910  seq1ublem 6911  cau2 6913  caure 6927  cauim 6928  ser1absdiflem 6929  facp1t 6936  facclt 6940  facdivt 6942  facwordit 6944  faclbnd 6945  faclbnd4lem1 6948  faclbnd4lem2 6949  faclbnd4lem3 6950  faclbnd4lem4 6951  bcvalt 6958  dffsum 6998  fsumserzf 7000  ser1ser0 7048  serzcl2t 7049  serz1p 7052  serzmulc 7058  serzrelem 7061  clm4at 7090  clmi2at 7091  climconst3 7096  climshft 7104  iserzshft2 7107  serzclim0 7109  climrecl 7110  climge0 7112  climaddlem1 7114  climaddlem3 7116  climmullem6 7125  climmullem8 7127  climsub 7130  climcmplem 7137  climabslem 7148  climubi 7153  climub 7154  climcau 7156  caucvglem2 7158  caucvg 7163  caucvg3 7167  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1const 7171  ser1cmp 7174  ser1cmp2 7177  iserzabs 7179  cvgcmp2lem 7180  cvgcmp2 7181  cvgcmp2c 7183  cvgcmp3ce 7187  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  isumvaltf 7193  isum1p 7206  isumnn0nna 7208  iserzgt0 7211  isummulc1 7212  isummulc1ALT 7213  isummulc1a 7214  isumcmpi 7215  reccnv 7218  expcnv 7233  geoser 7234  geolimi 7236  geolim 7237  geolim1 7239  geoisumr 7243  cvgratlem1ALT 7247  cvgratlem3ALT 7249  cvgratlem1 7250  cvgratlem3 7252  cvgratlem4 7253  negfcncf 7269  ivthlem4 7284  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  ivthlem9 7289  dsupivthlem 7291  efcltlem1 7304  dfef2 7307  ef0lem 7310  efclt 7312  efcvg 7314  eftval 7316  reefclt 7318  erelem3 7321  erelem6 7324  ege2lem2 7328  ege2le3lem2 7329  efcjt 7337  efaddlem6 7343  efaddt 7367  ef1tlub 7382  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  ef01tlub 7386  absef01tlub 7388  ef4pt 7400  efgt0 7404  efgt0t 7405  efltb 7407  reef11t 7409  eflegeot 7416  efm1legeot 7418  efcnlem4 7422  reeff1olem1 7424  reeff1o 7426  reefiso 7428  sinaddt 7453  cosaddt 7454  abseft 7483  acdc3lem 7486  acdc3 7487  acdclem 7494  acdc 7495  acdcALT 7496  ruclem4 7513  ruclem25 7534  ruclem29 7538  ruclem33 7542  ruclem35 7544  ruclem37 7546  infmap2lem2 7580  clsfval 7668  0ntr 7702  lpfval 7742  cnpval 7759  metxpdval 7829  metxp 7834  opnfval 7857  methaus 7882  metcni 7894  iscau3 7938  iscau4 7940  iscaunns 7944  iscms 7946  lmfexlem2 7957  lmle 7960  metelcls 7965  metcnp4lem1 7968  metcnp4lem2 7969  metcnp4 7970  metcn4i 7972  xplmi 7973  xplm 7975  xpcn 7976  bopcnlem2 7982  fsumcnlem 7989  lmcau 7996  bcthlem2 8000  bcthlem10 8008  bcthlem15 8013  bcthlem16 8014  bcthlem17 8015  bcthlem18 8016  bcthlem20 8018  bcthlem28 8026  bcthlem29 8027  bcthlem33 8031  bcth 8032  grpinvfval 8066  grpinvf 8079  grpdivfval 8081  grpdivval 8082  ghgrpilem1 8133  nvvcop 8213  bafval 8223  isnvlem 8229  nvi 8233  nvs 8290  nvz 8297  nvtri 8298  imsval 8316  imsmet 8324  sqcn 8335  nmcn 8339  ipfval 8352  iporthcom 8369  ip1cnilem2 8374  sspval 8382  isssp 8383  lnoval 8413  lnolin 8415  nmofval 8425  nmosetn0 8428  nmolb 8434  nmoubi 8435  nmobndseqi 8440  isblo 8442  0ofval 8447  nmo0 8451  nmlno0lem 8453  nmlno0i 8454  nmlnoubi 8456  lnon0 8458  nmblolbii 8459  nmblolbi 8460  blocnilem 8464  ajfval 8469  phpar2 8482  phpar 8483  ipdir 8502  ipass 8505  sii 8514  isbn 8524  ubthlem1 8529  ubthlem3 8531  minveclem6 8550  minveclem7 8551  minveclem8 8552  minveclem23 8567  minveclem27 8571  minveclem33 8577  minveceu 8583  htthlem2 8621  htthlem3 8622  htthlem4 8623  sincolem 8665  pilem1 8671  pilem2 8672  pilem3 8673  pilem4 8674  cosh111lem2 8715  cosh111t 8717  efif 8721  efifolem1 8722  efifolem2 8723  efifolem3 8724  efifolem6 8727  efifo 8729  efif1lem5 8734  efielcirc 8739  circgrp 8740  eff1i 8744  effoi 8745  pilog 8768  logltbt 8776  orthcom 8974  normlem7tALT 8985  normsqt 9001  norm-iit 9005  norm-iiit 9007  normpytht 9012  normpart 9022  bcsALT 9046  bcst 9048  hcau2 9055  hlimcaui 9106  norm1ex 9122  occllem3 9175  occllem5 9177  occlt 9182  projlem22 9207  projlem23 9208  projlem26 9211  pjthlem8 9226  pjtht 9234  pjtheut 9236  pjmvalt 9238  omls 9246  ococt 9248  axpjpjt 9256  pjoc1t 9267  pjomlt 9269  pjoc2t 9272  chocint 9418  chsscon3t 9423  chjot 9438  chdmm1t 9448  spanunt 9468  hosvalt 9516  hosvaltOLD 9517  homvalt 9518  hodvalt 9519  hodvaltOLD 9520  hfsvalt 9521  hfmvalt 9522  cmbrt 9527  pjoml6 9532  cmbr3t 9551  pjoml2t 9554  pjoml3t 9555  cmcm3t 9558  osumlem8 9585  osumt 9588  pjch1t 9615  pjadjt 9630  pjaddt 9631  pjinormt 9632  pjsubt 9633  pjmult 9634  pjige0t 9636  pjcjt2 9637  pjcht 9639  pjjs 9645  pjrn 9647  pjfot 9651  pj11 9656  pj11t 9659  pjopytht 9665  pjnormt 9669  pjpytht 9670  pjnelt 9671  adjsymt 9759  eigret 9761  eigortht 9764  elbdopt 9787  nmopsetn0 9792  nmfnsetn0 9805  eigvalvalt 9823  nmoplbt 9831  nmopubt 9832  cnopct 9837  lnoplt 9838  unopt 9839  hmopt 9846  nmfnlbt 9848  nmfnleubt 9849  elnlfnt 9852  cnfnct 9854  lnfnlt 9855  adjt 9857  eleigvect 9881  eigvalt 9884  nmop0 9910  nmfn0 9911  nmlnop0ALT 9920  nmlnop0t 9923  lnopeq0lem2 9931  lnopeq0 9932  lnopunilem1 9935  lnopuni 9937  elunop2t 9938  lnophmlem1 9941  lnophm 9943  lnophmt 9944  nmbdoplb 9949  nmbdoplbt 9950  nmcopexlem6 9956  nmcoplb 9958  nmcopext 9959  nmcoplbt 9960  nmophm 9961  lnopcon 9963  nmbdfnlb 9978  nmbdfnlbt 9979  nmcfnexlem6 9985  nmcfnlb 9987  nmcfnext 9988  nmcfnlbt 9989  lnfncon 9990  nlelch 9994  riesz3 9995  riesz1t 9998  cnlnadjlem1 10000  cnlnadjlem5 10004  adjbd1o 10018  adjeq0 10024  branmfnt 10038  rnbra 10040  pjbdln 10076  pjhmopt 10077  hmopidmch 10079  hmopidmpj 10080  pjss2co 10092  pjssmt 10093  pjssge0t 10094  pjdifnormt 10095  pjidmcot 10109  pjhmopidm 10110  elpjrncht 10118  pjin2 10121  pjclem1 10123  hstel2t 10146  stge0t 10151  stle1t 10152  hst1ht 10154  stjt 10162  strlem1 10177  strlem2 10178  hstrlem2 10186  stcltr1 10201  dmdmdt 10227  atordt 10315  irred 10321  mdsym 10338  cdj1 10360  cdj3lem1 10361  cdj3lem2a 10363  cdj3lem2b 10364  cdj3lem3a 10366  cdj3lem3b 10367  cdj3 10368  abs2sqlet 10374  abs2sqltt 10375  ghomgrpilem1 10385  ghomgrpilem2 10386  ghomsn 10388  ghomgrplem 10389  ghomlin 10393  ghomf1olem 10396  symggrp 10408  cayleylem2 10410  fveleq 10415  findreccl 10417  findabrcl 10418  sfvlim 10605  sfvlimOLD 10606  limfillem2OLD 10608  ist1 10614  eloi 10659  1ded 10671  idosd 10677  cmppfd 10678  domcmpd 10679  codcmpd 10680  cmpasso 10706  cmpida 10707  cmpidb 10708  ishoma 10715  ishomc 10717  ishomd 10718  eqidob 10723  ismona 10737  ismonb 10738  ismonb2 10740  isepia 10747  isepib 10748  isepib2 10750  isfuna 10754  idfisf 10760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-xp 3184  df-cnv 3186  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fv 3198

Copyright terms: Public domain