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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 6157 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 623 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶)))
3 df-f 6071 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
4 df-f 6071 . 2 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
52, 3, 43bitr4g 305 1 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wss 3731  ran crn 5277   Fn wfn 6062  wf 6063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2757  df-fn 6070  df-f 6071
This theorem is referenced by:  feq23  6206  feq2d  6208  feq2i  6214  f00  6268  f0dom0  6270  f1eq2  6278  fressnfv  6618  mapvalg  8069  map0g  8100  ac6sfi  8410  cofsmo  9343  axcc4dom  9515  ac6sg  9562  isghm  17925  pjdm2  20330  cmpcovf  21473  ulmval  24424  measval  30642  isrnmeas  30644  poseq  32128  soseq  32129  elno2  32182  noreson  32188  bj-finsumval0  33513  mbfresfi  33811  stoweidlem62  40848  hoidmvval0b  41376  vonioo  41468  vonicc  41471
  Copyright terms: Public domain W3C validator