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

Theorem fneq2 5894
 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 2621 . . 3 (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵))
21anbi2d 736 . 2 (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)))
3 df-fn 5807 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
4 df-fn 5807 . 2 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
52, 3, 43bitr4g 302 1 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  dom cdm 5038  Fun wfun 5798   Fn wfn 5799 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fn 5807 This theorem is referenced by:  fneq2d  5896  fneq2i  5900  feq2  5940  foeq2  6025  f1o00  6083  eqfnfv2  6220  wfrlem1  7301  wfrlem15  7316  tfrlem12  7372  ixpeq1  7805  ac5  9182  0fz1  12232  esumcvgsum  29477  bnj90  30042  bnj919  30091  bnj535  30214  bnj1463  30377  frrlem1  31024  fnchoice  38211
 Copyright terms: Public domain W3C validator