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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 6415 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 632 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶)))
3 df-f 6328 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
4 df-f 6328 . 2 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
52, 3, 43bitr4g 317 1 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ⊆ wss 3881  ran crn 5520   Fn wfn 6319  ⟶wf 6320 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fn 6327  df-f 6328 This theorem is referenced by:  feq23  6471  feq2d  6473  feq2i  6479  f00  6535  f0dom0  6537  f1eq2  6545  fressnfv  6899  mapvalg  8399  map0g  8431  ac6sfi  8746  cofsmo  9680  axcc4dom  9852  ac6sg  9899  isghm  18350  pjdm2  20400  cmpcovf  21996  ulmval  24975  measval  31567  isrnmeas  31569  poseq  33208  soseq  33209  elno2  33274  noreson  33280  bj-finsumval0  34700  mbfresfi  35103  stoweidlem62  42702  hoidmvval0b  43227  vonioo  43319  vonicc  43322
 Copyright terms: Public domain W3C validator