Theorem fveq1 3714

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

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

This theorem is referenced by:  fveq1i 3716  fveq1d 3717  eqfnfv 3788  isoeq1 3878  tfrlem3 3904  tfrlem12 3913  tz7.44-2 3920  rdgeq1 3925  rdglem2 3929  opreq 3958  omv 4141  oev 4143  elixp2 4339  mapsnen 4416  mapenlem2 4476  mapxpen 4481  aceq4 4714  aceq5lem5 4719  aceq6a 4721  ac6lem 4734  seq1val 6257  shftfval 6287  clim 6923  climfnn 7038  caucvg3t 7112  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  elcncf 7208  abspef01tlub 7344  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  iscnp 7710  lmbr 7880  iscau 7888  metcn4i 7922  bcth 7982  isnvlem 8181  nvi 8185  islno 8361  nmoval 8371  nmblolbi 8404  isphg 8420  ajmoi 8463  ubthi 8488  hcau 8990  hlim 8995  hlim2 8999  hosmvalt 9451  hommvalt 9452  hodmvalt 9453  hfsmvalt 9454  hfmmvalt 9455  adjmo 9698  nmopvalt 9722  elcnopt 9723  ellnopt 9724  elunopt 9739  elhmopt 9740  nmfnvalt 9743  nlfnvalt 9748  elcnfnt 9749  ellnfnt 9750  adjvalt 9754  eigvecvalt 9762  eigvalvalt 9763  adjt 9796  adjeqt 9798  hmopadj2t 9804  lnopeq0 9870  lnopeqt 9872  elunop2t 9876  lnophmt 9882  hmopcot 9886  nmbdoplbt 9888  nmcoplbt 9898  lnopcont 9902  lnfn0t 9914  lnfnmult 9915  nmbdfnlbt 9917  nmcfnlbt 9927  lnfncont 9929  riesz4t 9935  riesz1t 9936  cnlnadjlem9 9946  cnlnadjeut 9949  cnlnssadj 9951  nmopco 9966  bra11 9979  cnvbravalt 9981  hmopidmcht 10019  hmopidmpjt 10020  pjss2co 10030  pjssdif2 10040  pjssdif1 10041  pjclem4 10065  pj3s 10073  pj3cor1 10075  stelt 10079  hstelt 10080  str 10122  hstr 10130  elghomlem2 10317  cayleylem3 10345  isded 10549  dedi 10550  iscat 10567  cati 10568  isfunb 10629

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-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193

Copyright terms: Public domain