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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 6661 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 631 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶)))
3 df-f 6567 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
4 df-f 6567 . 2 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wss 3963  ran crn 5690   Fn wfn 6558  wf 6559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fn 6566  df-f 6567
This theorem is referenced by:  feq23  6720  feq2d  6723  feq2i  6729  f00  6791  f0dom0  6793  f1eq2  6801  fressnfv  7180  poseq  8182  soseq  8183  mapvalg  8875  fsetexb  8903  map0g  8923  ac6sfi  9318  cofsmo  10307  axcc4dom  10479  ac6sg  10526  isghm  19246  isghmOLD  19247  pjdm2  21749  cmpcovf  23415  ulmval  26438  elno2  27714  noreson  27720  measval  34179  isrnmeas  34181  bj-finsumval0  37268  mbfresfi  37653  sn-isghm  42660  dfno2  43418  stoweidlem62  46018  hoidmvval0b  46546  vonioo  46638  vonicc  46641  f102g  48682  f1mo  48683
  Copyright terms: Public domain W3C validator