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

Theorem fneq2 6661
Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fneq2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))

Proof of Theorem fneq2
StepHypRef Expression
1 eqeq2 2747 . . 3 (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵))
21anbi2d 630 . 2 (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)))
3 df-fn 6566 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
4 df-fn 6566 . 2 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  dom cdm 5689  Fun wfun 6557   Fn wfn 6558
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
This theorem is referenced by:  fneq2d  6663  fneq2i  6667  feq2  6718  foeq2  6818  f1o00  6884  eqfnfv2  7052  frrlem1  8310  frrlem13  8322  wfrlem1OLD  8347  wfrlem15OLD  8362  tfrlem12  8428  ixpeq1  8947  ac5  10515  0fz1  13581  esumcvgsum  34069  bnj90  34715  bnj919  34760  bnj535  34883  bnj1463  35048  fnchoice  44967
  Copyright terms: Public domain W3C validator