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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 6660 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 631 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶)))
3 df-f 6565 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
4 df-f 6565 . 2 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wss 3951  ran crn 5686   Fn wfn 6556  wf 6557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-fn 6564  df-f 6565
This theorem is referenced by:  feq23  6719  feq2d  6722  feq2i  6728  f00  6790  f0dom0  6792  f1eq2  6800  fressnfv  7180  poseq  8183  soseq  8184  mapvalg  8876  fsetexb  8904  map0g  8924  ac6sfi  9320  cofsmo  10309  axcc4dom  10481  ac6sg  10528  isghm  19233  isghmOLD  19234  pjdm2  21731  cmpcovf  23399  ulmval  26423  elno2  27699  noreson  27705  measval  34199  isrnmeas  34201  bj-finsumval0  37286  mbfresfi  37673  sn-isghm  42683  dfno2  43441  relpeq4  44968  stoweidlem62  46077  hoidmvval0b  46605  vonioo  46697  vonicc  46700  f102g  48761  f1mo  48762
  Copyright terms: Public domain W3C validator