MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq3 Structured version   Visualization version   GIF version

Theorem feq3 6239
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
feq3 (𝐴 = 𝐵 → (𝐹:𝐶𝐴𝐹:𝐶𝐵))

Proof of Theorem feq3
StepHypRef Expression
1 sseq2 3823 . . 3 (𝐴 = 𝐵 → (ran 𝐹𝐴 ↔ ran 𝐹𝐵))
21anbi2d 623 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵)))
3 df-f 6105 . 2 (𝐹:𝐶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐴))
4 df-f 6105 . 2 (𝐹:𝐶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵))
52, 3, 43bitr4g 306 1 (𝐴 = 𝐵 → (𝐹:𝐶𝐴𝐹:𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  wss 3769  ran crn 5313   Fn wfn 6096  wf 6097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-in 3776  df-ss 3783  df-f 6105
This theorem is referenced by:  feq23  6240  feq3d  6243  fun2  6282  fconstg  6307  f1eq3  6313  mapvalg  8105  mapsnd  8137  cantnff  8821  axdc4uz  13038  supcvg  14926  lmff  21434  txcn  21758  lmmbr  23384  iscmet3  23419  dvcnvrelem2  24122  itgsubstlem  24152  umgrislfupgr  26358  usgrislfuspgr  26420  wlkv0  26900  isgrpo  27877  vciOLD  27941  isvclem  27957  nmop0h  29375  sitgaddlemb  30926  sitmcl  30929  cvmliftlem15  31797  mtyf  31966  matunitlindflem1  33894  sdclem1  34026  k0004lem1  39227  stoweidlem57  41017  isomushgr  42496
  Copyright terms: Public domain W3C validator