Theorem fveq1 4680

Description: Equality theorem for function value.

Assertion

Ref	Expression
fveq1	|- (F = G -> (F` A) = (G` A))

Proof of Theorem fveq1

Step	Hyp	Ref	Expression
1		imaeq1 4259	. . . . 5 |- (F = G -> (F"{A}) = (G"{A}))
2	1	eqeq1d 1892	. . . 4 |- (F = G -> ((F"{A}) = {x} <-> (G"{A}) = {x}))
3	2	abbidv 2008	. . 3 |- (F = G -> {x | (F"{A}) = {x}} = {x | (G"{A}) = {x}})
4	3	unieqd 3188	. 2 |- (F = G -> U.{x | (F"{A}) = {x}} = U.{x | (G"{A}) = {x}})
5		df-fv 4014	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
6		df-fv 4014	. 2 |- (G` A) = U.{x | (G"{A}) = {x}}
7	4, 5, 6	3eqtr4g 1953	1 |- (F = G -> (F` A) = (G` A))

Syntax hints:   -> wi 3   = wceq 1298  {cab 1871  {csn 3044  U.cuni 3177  "cima 3989  ` cfv 3998

This theorem is referenced by:  fveq1i 4682  fveq1d 4683  eqfnfv 4766  isoeq1 4863  opreq 4888  tfrlem3 5121  tfrlem12 5130  tz7.44-2 5137  rdgeq1 5142  rdglem2 5146  omv 5196  oev 5198  elixp2 5408  mapsnen 5488  ac6sfilem1 5506  mapenlem2 5584  mapxpen 5589  aceq4 5896  aceq5lem5 5901  aceq6a 5903  ac6lem 5916  seq1val 7725  shftfval 7755  clim 8237  climfnn 8352  caucvg3 8428  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  elcncf 8527  abspef01tlubi 8660  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  iscnp 9036  lmbr 9206  iscau 9214  metcn4i 9250  bcth 9310  isnvlem 9561  nvi 9565  vacnlem4 9670  islno 9753  nmoval 9765  nmblolbi 9800  isphg 9817  ajmoi 9860  ajval 9863  ubthi 9889  elghomlem2 10194  upxp 10225  hcau 10684  hlimi 10689  hlim2 10693  hosmval 11144  hommval 11145  hodmval 11146  hfsmval 11147  hfmmval 11148  adjmo 11395  nmopval 11419  elcnop 11420  ellnop 11421  elunop 11436  elhmop 11437  nmfnval 11440  nlfnval 11445  elcnfn 11446  ellnfn 11447  adjval 11451  eigvecval 11459  eigvalval 11460  adj1 11494  adjeq 11496  hmopadj2 11502  lnopeq0i 11569  lnopeq 11571  elunop2 11575  lnophm 11581  hmopco 11585  nmbdoplb 11587  nmcoplb 11597  lnopcon 11601  lnfn0 11613  lnfnmul 11614  nmbdfnlb 11616  nmcfnlb 11626  lnfncon 11628  riesz4 11634  riesz1 11635  cnlnadjlem9 11645  cnlnadjeu 11648  cnlnssadj 11650  nmopcoi 11665  bra11 11679  cnvbraval 11681  hmopidmch 11725  hmopidmpj 11726  pjss2coi 11736  pjssdif2i 11746  pjssdif1i 11747  pjclem4 11772  pj3si 11780  pj3cor1i 11782  stel 11786  hstel 11787  stri 11829  hstri 11837  bnj64 13201  bnj104 13224  bnj106 13225  bnj149 13241  bnj154 13245  bnj155 13246  bnj526 13263  bnj540 13267  bnj609 13306  bnj611 13307  bnj891 13321  bnj892 13322  bnj965 13346  bnj1000 13364  bnj1014 13374  bnj1015 13375  bnj1234 13460  bnj1463 13550  cayleylem3 13643  poseq 13954  soseq 13955  wfrlem1 13957  wfrlem15 13971  sltval 13988  axfelem5 14035  surrc2 14390  eqfnung2 14459  injrec 14461  surjsec 14462  fopab2g 14485  elixp2b 14494  valpr 14499  repcpwti 14503  cbicplem 14508  cbicp 14509  fprodneg 14741  svli2 14826  istopx 14918  isded 15083  dedi 15084  iscat 15101  cati 15102  isfunb 15183  cocanfo 15689  eqfnun 15705  upixp 15729  seq11g 15804  seq1p1g 15805  seqz1g 15806  seqzp1g 15807  sdc 15811  fdc 15812  fsumltisumi 15823  fsumleisumi 15826  iserzshft2 15829  isumshft2 15830  trirn 15834  mettrifi2 15848  tlmbr 15904  isismty 15948  bfplem11 16008  rrnmval 16014  rrntotbndlem1 16020  phtpyval 16047  isphtpc 16059  reparpht 16065  pcoval 16073  pcoloopf 16079  elpi1i 16090  pi1bvalqs 16091  pi1f 16093  pi1val 16094  isrnghom 16119  smoeq 16444  addrval 16466  subrval 16467  mulvval 16468  eustrdif 16722  stbval 16731  strcval 16732  stb2xpl 16742  stb3xpl 16743  isopos 16909  issrng 17176  isphil 17195  ispaut 17396  isdil 17403  istrn 17406

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014

Copyright terms: Public domain