Theorem fveq2 2832

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 1816	. . . . . 6 |- (A = B -> {A} = {B})
2		imaeq2 2603	. . . . . 6 |- ({A} = {B} -> (F"{A}) = (F"{B}))
3	1, 2	syl 12	. . . . 5 |- (A = B -> (F"{A}) = (F"{B}))
4	3	cleq1d 1109	. . . 4 |- (A = B -> ((F"{A}) = {x} <-> (F"{B}) = {x}))
5	4	biabdv 1183	. . 3 |- (A = B -> {x | (F"{A}) = {x}} = {x | (F"{B}) = {x}})
6	5	unieqd 1929	. 2 |- (A = B -> U.{x | (F"{A}) = {x}} = U.{x | (F"{B}) = {x}})
7		df-fv 2438	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
8		df-fv 2438	. 2 |- (F` B) = U.{x | (F"{B}) = {x}}
9	6, 7, 8	3eqtr4g 1147	1 |- (A = B -> (F` A) = (F` B))

Syntax hints:   -> wi 2  {cab 1090   = wceq 1091  {csn 1808  U.cuni 1919  "cima 2413  ` cfv 2422

This theorem is referenced by:  fveq2i 2835  fveq2d 2836  tz6.12-2 2845  funbrfv 2852  fnfvbr 2855  fnopabfv 2858  cleqfvf 2881  elrnopab 2884  fvrn 2888  fnressn 2897  fressnfv 2898  fvi 2900  fconstfv 2903  fvresex 2909  abrexexlem2 2911  f1fvf 2917  f1fveq 2918  f1ocnvfv 2921  f1ocnvfvb 2922  isorel 2932  isocnv 2934  isotr 2935  isotrALT 2936  f1owe 2943  f1oweOLD 2944  canth 2945  tfrlem1 2949  tfrlem2 2950  tfrlem11 2959  tfr2 2963  tfr3 2964  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  rdglem1 2975  rdglem2 2976  rdgsuct 2983  rdglimt 2986  tz7.48lem 2993  tz7.49 2997  abianfplem 2999  abianfp 3000  ffnoprval 3041  fnoprval 3042  elrnoprab 3054  oprvalex 3055  1st2val 3097  df1st2 3098  oav 3119  omv 3120  oev 3122  omsmolem 3195  dom2d 3307  mapenlem2 3385  unblem2 3432  inf3lemd 3463  inf3lem1 3464  inf3lem2 3465  inf3lem5 3468  trcl 3489  r1tr 3498  r1ord 3499  r1ord3 3501  r1val1 3502  tz9.12lem3 3505  tz9.12 3506  rankvalg 3513  rankr1 3518  rankr1g 3519  r1pwcl 3530  ranksn 3532  rankonid 3538  rankr1id 3539  scottex 3541  scott0 3542  scottexs 3543  scott0s 3544  karden 3551  aceq3lem 3555  aceq4 3557  aceq5 3563  aceq6b 3565  ac6lem 3575  numthlem 3598  numth 3599  zornlem6 3608  oncard 3636  carduni 3664  cardiun 3665  cardprc 3667  alephon 3671  alephcard 3673  alephordlem2 3678  alephordi 3679  alephord 3680  alephle 3689  cardaleph 3690  cardalephex 3691  cf0 3705  cardcf 3706  cflecard 3707  cfsuc 3709  reclem1pr 3950  reclem2pr 3951  reclem3pr 3952  om2uzsuc 4652  om2uzuz 4653  om2uzlt 4654  seqlem1 4662  seqrval 4664  seqval2 4667  seqsuclem 4669  seqrn 4673  expvalt 4677  sqrth 4757  sqrcl 4758  sqrgt0 4759  sqrge0 4760  sqr11 4761  sqrmul 4763  sqrclt 4767  sqrgt0t 4768  sqrge0t 4769  sqr00t 4770  sqsqrt 4776  cjvalt 4799  absvalt 4801  cjret 4829  cjcjt 4830  cjaddt 4831  cjmult 4832  abs00 4839  absclt 4848  absmult 4849  absltt 4857  absidt 4862  absgt0t 4863  abslem2 4867  facp1t 4873  facclt 4874  ruclem4 4888  ruclem25 4909  ruclem29 4913  ruclem33 4917  ruclem35 4919  ruclem37 4921  infmap2lem2 4952  hiidrclt 5053  orthcom 5061  normlem7t 5072  norm-iiit 5088  normpytht 5092  bcs 5101  hlimcaui 5141  occllem3 5182  occllem5 5184  occlt 5189  projlem22 5214  projlem23 5215  projlem26 5218  pjthlem8 5232  pjtht 5240  pjthut 5243  pjmvalt 5245  omls 5251  ococt 5253  axpjpjt 5260  pjoc1t 5270  pjoc2t 5274  chsscon3t 5417  chdmm1t 5438  hosvalt 5489  hodvalt 5490  cmbrt 5494  pjoml5 5498  pjoml3t 5517  osumlem8 5537  pjch1t 5560  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcjt2 5580  pjcht 5582  pjjs 5585  pjrn 5587  pj11 5591  pjss2co 5634  pjssmt 5635  pjssge0t 5636  pjdifnormt 5637  pjin2 5647  pjclem1 5649  pjopytht 5662  pjnormt 5666  pjnelt 5667  stge0t 5673  stle1t 5674  stjt 5676  strlem1 5691  strlem2 5692  stcltr1 5707  dmdbr 5731  mdsym 5784

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438

metamath.org