Theorem fveq2 3731

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 2422	. . . . . 6 |- (A = B -> {A} = {B})
2	1	imaeq2d 3411	. . . . 5 |- (A = B -> (F"{A}) = (F"{B}))
3	2	eqeq1d 1486	. . . 4 |- (A = B -> ((F"{A}) = {x} <-> (F"{B}) = {x}))
4	3	abbidv 1580	. . 3 |- (A = B -> {x | (F"{A}) = {x}} = {x | (F"{B}) = {x}})
5	4	unieqd 2517	. 2 |- (A = B -> U.{x | (F"{A}) = {x}} = U.{x | (F"{B}) = {x}})
6		df-fv 3205	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
7		df-fv 3205	. 2 |- (F` B) = U.{x | (F"{B}) = {x}}
8	5, 6, 7	3eqtr4g 1534	1 |- (A = B -> (F` A) = (F` B))

Syntax hints:   -> wi 3   = wceq 958  {cab 1466  {csn 2414  U.cuni 2508  "cima 3180  ` cfv 3189

This theorem is referenced by:  fveq2i 3734  fveq2d 3735  tz6.12-2 3746  funbrfv 3757  fnbrfvb 3760  fnopabfv 3765  ssimaex 3775  eqfnfvf 3805  elrnopabg 3807  fvelrn 3819  ffnfvf 3836  fnressn 3844  fressnfv 3845  fopabsn 3847  fvi 3849  fconstfv 3856  fvresex 3864  abrexexlem2 3866  funiunfv 3873  funiunfvf 3877  f1fvf 3882  f1fveq 3883  f1ocnvfv 3887  f1ocnvfvb 3888  f1ocnvfv3 3890  isorel 3901  isocnv 3903  isotr 3904  isotrALT 3905  f1owe 3912  f1oweALT 3913  canth 3914  tfrlem1 3918  tfrlem2 3919  tfrlem11 3928  tfr2 3932  tfr3 3933  tz7.44-1 3935  tz7.44-2 3936  tz7.44-3 3937  rdglem1 3944  rdglem2 3945  rdgsuct 3952  rdglimt 3955  tz7.48lem 3962  tz7.49 3966  abianfplem 3968  abianfp 3969  ffnoprval 4021  eqfnoprval 4023  fnoprval 4024  fnrnoprval 4043  fooprval 4044  oprvalex 4048  1stval2 4096  2ndval2 4097  1st2val 4102  2nd2val 4103  2ndconst 4104  eqop 4111  unielxp 4114  sbcopeq1a 4118  csbopeq1a 4119  dfopab2 4120  dfoprab3 4121  dfoprab4 4123  elrnoprabg 4131  df1st2 4133  df2nd2 4134  oav 4157  omv 4158  oev 4160  oev2 4169  omsmolem 4263  dom2d 4411  mapenlem2 4497  unblem2 4554  inf3lemd 4628  inf3lem1 4629  inf3lem2 4630  inf3lem5 4633  trcl 4662  r1tr 4671  r1ord 4672  r1ord3 4674  r1val1 4675  tz9.12lem3 4678  tz9.12 4679  rankvalg 4686  rankr1 4691  rankr1g 4692  ranklim 4702  r1pwcl 4704  ranksn 4706  rankonid 4712  rankeq0 4713  rankr1id 4714  rankuni 4715  rankxplim 4729  scottex 4733  scott0 4734  scottexs 4735  scott0s 4736  karden 4743  aceq3lem 4749  aceq4 4751  aceq5 4757  aceq6b 4759  ac6lem 4771  numthlem 4800  numth 4801  zorn2lem6 4810  unidom 4825  uniimadomf 4828  oncard 4846  carduni 4876  cardiun 4877  cardprc 4879  alephon 4883  alephcard 4885  alephordlem2 4891  alephordi 4892  alephord 4893  alephle 4902  cardaleph 4903  cardalephex 4904  alephfplem2 4915  alephfplem3 4916  alephfplem4 4917  alephfp2 4919  alephval2 4920  alephval3 4921  cf0 4929  cardcf 4930  cflecard 4931  cfeq0 4933  cfsuc 4934  reclem1pr 5175  reclem2pr 5176  reclem3pr 5177  monoord 6302  om2uzsuc 6304  om2uzuz 6305  om2uzlt 6306  om2uzlt2 6307  seq1lem1 6317  seq1rval 6319  seq1val2 6322  seq1suclem 6324  seq1rn2 6329  seq1res 6335  ser1recl 6339  ser1mono 6345  ser1add2 6346  ser1add 6347  seq1shftid 6364  icoshftf1oi 6417  uz11t 6440  fsequb 6531  seqzfval 6545  seqzfveq 6562  seqzrn2 6564  seqzres2 6569  ser0cl1 6572  expvalt 6578  sqrth 6707  sqrcl 6708  sqrgt0 6709  sqrge0 6710  sqr11 6711  sqrmul 6713  sqrclt 6718  sqrgt0t 6719  sqrge0t 6720  sqrlet 6721  sqr00t 6722  sqsqrt 6731  absvalt 6770  cjvalt 6771  cjrebt 6807  cjmulrclt 6808  cjmulvalt 6809  cjmulge0t 6810  renegt 6811  readdt 6812  imnegt 6814  imaddt 6815  cjcjt 6818  cjaddt 6819  cjmult 6820  cjnegt 6821  addcjt 6822  abs00 6849  absval2t 6859  abs00t 6860  absge0t 6861  absmult 6865  absdivt 6867  absidt 6869  absltt 6887  abslet 6888  abssubne0t 6889  cjdivt 6896  absgt0t 6900  abstrit 6905  abs1m 6911  abslem2 6916  seq1bnd 6917  seq1ublem 6918  cau2 6920  caure 6934  cauim 6935  ser1absdiflem 6936  facp1t 6943  facclt 6947  facdivt 6949  facwordit 6951  faclbnd 6952  faclbnd4lem1 6955  faclbnd4lem2 6956  faclbnd4lem3 6957  faclbnd4lem4 6958  bcvalt 6965  dffsum 7005  fsumserzf 7007  ser1ser0 7055  serzcl2t 7056  serz1p 7059  serzmulc 7065  serzrelem 7068  clm4at 7097  clmi2at 7098  climconst3 7103  climshft 7111  iserzshft2 7114  serzclim0 7116  climrecl 7117  climge0 7119  climaddlem1 7121  climaddlem3 7123  climmullem6 7132  climmullem8 7134  climsub 7137  climcmplem 7144  climabslem 7155  climubi 7160  climub 7161  climcau 7163  caucvglem2 7165  caucvg 7170  caucvg3 7174  caucvg3t 7175  serzf0 7176  ser1f0 7177  ser1const 7178  ser1cmp 7181  ser1cmp2 7184  iserzabs 7186  cvgcmp2lem 7187  cvgcmp2 7188  cvgcmp2c 7190  cvgcmp3ce 7194  cvgcmp3cetlem1 7195  cvgcmp3cetlem2 7196  isumvaltf 7200  isum1p 7213  isumnn0nna 7215  iserzgt0 7218  isummulc1 7219  isummulc1ALT 7220  isummulc1a 7221  isumcmpi 7222  reccnv 7225  expcnv 7240  geoser 7241  geolimi 7243  geolim 7244  geolim1 7246  geoisumr 7250  cvgratlem1ALT 7254  cvgratlem3ALT 7256  cvgratlem1 7257  cvgratlem3 7259  cvgratlem4 7260  negfcncf 7276  ivthlem4 7291  ivthlem6 7293  ivthlem7 7294  ivthlem8 7295  ivthlem9 7296  dsupivthlem 7298  efcltlem1 7311  dfef2 7314  ef0lem 7317  efclt 7319  efcvg 7321  eftval 7323  reefclt 7325  erelem3 7328  erelem6 7331  ege2lem2 7335  ege2le3lem2 7336  efcjt 7344  efaddlem6 7350  efaddt 7374  ef1tlub 7389  ef01tllem1 7390  ef01tllem2 7391  ef01tllem2OLD 7392  ef01tlub 7393  absef01tlub 7395  ef4pt 7407  efgt0 7411  efgt0t 7412  efltb 7414  reef11t 7416  eflegeot 7423  efm1legeot 7425  efcnlem4 7429  reeff1olem1 7431  reeff1o 7433  reefiso 7435  sinaddt 7460  cosaddt 7461  abseft 7491  acdc3lem 7494  acdc3 7495  acdclem 7502  acdc 7503  acdcALT 7504  ruclem4 7521  ruclem25 7542  ruclem29 7546  ruclem33 7550  ruclem35 7552  ruclem37 7554  infmap2lem2 7589  clsfval 7672  0ntr 7706  lpfval 7746  cnpval 7763  metxpdval 7833  metxp 7838  opnfval 7861  methaus 7886  metcni 7898  iscau3 7942  iscau4 7944  iscaunns 7948  iscms 7950  lmfexlem2 7961  lmle 7964  metelcls 7969  metcnp4lem1 7972  metcnp4lem2 7973  metcnp4 7974  metcn4i 7976  xplmi 7977  xplm 7979  xpcn 7980  bopcnlem2 7986  fsumcnlem 7993  lmcau 8000  bcthlem2 8004  bcthlem10 8012  bcthlem15 8017  bcthlem16 8018  bcthlem17 8019  bcthlem18 8020  bcthlem20 8022  bcthlem28 8030  bcthlem29 8031  bcthlem33 8035  bcth 8036  grpinvfval 8069  grpinvf 8082  grpdivfval 8084  grpdivval 8085  ghgrpilem1 8136  nvvcop 8216  bafval 8226  isnvlem 8232  nvi 8236  nvs 8293  nvz 8300  nvtri 8301  imsval 8319  imsmet 8327  sqcn 8338  nmcn 8342  ipfval 8355  iporthcom 8372  ip1cnilem2 8377  sspval 8385  isssp 8386  lnoval 8416  lnolin 8418  nmofval 8428  nmosetn0 8431  nmolb 8437  nmoubi 8438  nmobndseqi 8443  isblo 8445  0ofval 8450  nmo0 8454  nmlno0lem 8456  nmlno0i 8457  nmlnoubi 8459  lnon0 8461  nmblolbii 8462  nmblolbi 8463  blocnilem 8467  ajfval 8472  phpar2 8485  phpar 8486  ipdir 8505  ipass 8508  sii 8517  isbn 8527  ubthlem1 8532  ubthlem3 8534  minveclem6 8553  minveclem7 8554  minveclem8 8555  minveclem23 8570  minveclem27 8574  minveclem33 8580  minveceu 8586  htthlem2 8624  htthlem3 8625  htthlem4 8626  sincolem 8667  pilem1 8673  pilem2 8674  pilem3 8675  pilem4 8676  cosh111lem2 8717  cosh111t 8719  efif 8723  efifolem1 8724  efifolem2 8725  efifolem3 8726  efifolem6 8729  efifo 8731  efif1lem5 8736  efielcirc 8741  circgrp 8742  eff1i 8746  effoi 8747  pilog 8770  logltbt 8778  orthcom 8976  normlem7tALT 8987  normsqt 9003  norm-iit 9007  norm-iiit 9009  normpytht 9014  normpart 9024  bcsALT 9048  bcst 9050  hcau2 9057  hlimcaui 9108  norm1ex 9124  occllem3 9177  occllem5 9179  occlt 9184  projlem22 9209  projlem23 9210  projlem26 9213  pjthlem8 9228  pjtht 9236  pjtheut 9238  pjmvalt 9240  omls 9248  ococt 9250  axpjpjt 9258  pjoc1t 9269  pjomlt 9271  pjoc2t 9274  chocint 9420  chsscon3t 9425  chjot 9440  chdmm1t 9450  spanunt 9470  hosvalt 9518  hosvaltOLD 9519  homvalt 9520  hodvalt 9521  hodvaltOLD 9522  hfsvalt 9523  hfmvalt 9524  cmbrt 9529  pjoml6 9534  cmbr3t 9553  pjoml2t 9556  pjoml3t 9557  cmcm3t 9560  osumlem8 9587  osumt 9590  pjch1t 9617  pjadjt 9632  pjaddt 9633  pjinormt 9634  pjsubt 9635  pjmult 9636  pjige0t 9638  pjcjt2 9639  pjcht 9641  pjjs 9647  pjrn 9649  pjfot 9653  pj11 9658  pj11t 9661  pjopytht 9667  pjnormt 9671  pjpytht 9672  pjnelt 9673  adjsymt 9761  eigret 9763  eigortht 9766  elbdopt 9789  nmopsetn0 9794  nmfnsetn0 9807  eigvalvalt 9825  nmoplbt 9833  nmopubt 9834  cnopct 9839  lnoplt 9840  unopt 9841  hmopt 9848  nmfnlbt 9850  nmfnleubt 9851  elnlfnt 9854  cnfnct 9856  lnfnlt 9857  adjt 9859  eleigvect 9883  eigvalt 9886  nmop0 9912  nmfn0 9913  nmlnop0ALT 9922  nmlnop0t 9925  lnopeq0lem2 9933  lnopeq0 9934  lnopunilem1 9937  lnopuni 9939  elunop2t 9940  lnophmlem1 9943  lnophm 9945  lnophmt 9946  nmbdoplb 9951  nmbdoplbt 9952  nmcopexlem6 9958  nmcoplb 9960  nmcopext 9961  nmcoplbt 9962  nmophm 9963  lnopcon 9965  nmbdfnlb 9980  nmbdfnlbt 9981  nmcfnexlem6 9987  nmcfnlb 9989  nmcfnext 9990  nmcfnlbt 9991  lnfncon 9992  nlelch 9996  riesz3 9997  riesz1t 10000  cnlnadjlem1 10002  cnlnadjlem5 10006  adjbd1o 10020  adjeq0 10026  branmfnt 10040  rnbra 10042  pjbdln 10078  pjhmopt 10079  hmopidmch 10081  hmopidmpj 10082  pjss2co 10094  pjssmt 10095  pjssge0t 10096  pjdifnormt 10097  pjidmcot 10111  pjhmopidm 10112  elpjrncht 10121  pjin2 10124  pjclem1 10126  hstel2t 10149  stge0t 10154  stle1t 10155  hst1ht 10157  stjt 10165  strlem1 10180  strlem2 10181  hstrlem2 10189  stcltr1 10204  dmdmdt 10230  atordt 10318  irred 10324  mdsym 10341  cdj1 10363  cdj3lem1 10364  cdj3lem2a 10366  cdj3lem2b 10367  cdj3lem3a 10369  cdj3lem3b 10370  cdj3 10371  abs2sqlet 10377  abs2sqltt 10378  ghomgrpilem1 10388  ghomgrpilem2 10389  ghomsn 10391  ghomgrplem 10392  ghomlin 10396  ghomf1olem 10399  symggrp 10411  cayleylem2 10413  fveleq 10418  findreccl 10420  findabrcl 10421  sfvlim 10584  sfvlimOLD 10585  limfillem2OLD 10587  ist1 10593  eloi 10638  1ded 10650  idosd 10656  cmppfd 10657  domcmpd 10658  codcmpd 10659  cmpasso 10685  cmpida 10686  cmpidb 10687  ishoma 10694  ishomc 10696  ishomd 10697  eqidob 10702  ismona 10716  ismonb 10717  ismonb2 10719  isepia 10726  isepib 10727  isepib2 10729  isfuna 10733  idfisf 10739

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709  ax-pow 2749  ax-pr 2786

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-nul 2285  df-pw 2407  df-sn 2417  df-pr 2418  df-op 2421  df-uni 2509  df-br 2626  df-opab 2673  df-xp 3191  df-cnv 3193  df-dm 3195  df-rn 3196  df-res 3197  df-ima 3198  df-fv 3205

Copyright terms: Public domain