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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 6307 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 629 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶)))
3 df-f 6221 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
4 df-f 6221 . 2 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
52, 3, 43bitr4g 315 1 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1520  wss 3854  ran crn 5436   Fn wfn 6212  wf 6213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-9 2089  ax-ext 2767
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786  df-fn 6220  df-f 6221
This theorem is referenced by:  feq23  6358  feq2d  6360  feq2i  6366  f00  6421  f0dom0  6423  f1eq2  6431  fressnfv  6776  mapvalg  8257  map0g  8288  ac6sfi  8598  cofsmo  9526  axcc4dom  9698  ac6sg  9745  isghm  18087  pjdm2  20525  cmpcovf  21671  ulmval  24639  measval  31030  isrnmeas  31032  poseq  32649  soseq  32650  elno2  32715  noreson  32721  bj-finsumval0  34065  mbfresfi  34415  stoweidlem62  41843  hoidmvval0b  42368  vonioo  42460  vonicc  42463
  Copyright terms: Public domain W3C validator