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

Theorem fneq2 6133
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 2763 . . 3 (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵))
21anbi2d 742 . 2 (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)))
3 df-fn 6044 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
4 df-fn 6044 . 2 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
52, 3, 43bitr4g 303 1 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  dom cdm 5258  Fun wfun 6035   Fn wfn 6036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-cleq 2745  df-fn 6044
This theorem is referenced by:  fneq2d  6135  fneq2i  6139  feq2  6180  foeq2  6265  f1o00  6324  eqfnfv2  6467  wfrlem1  7575  wfrlem15  7590  tfrlem12  7646  ixpeq1  8077  ac5  9483  0fz1  12546  esumcvgsum  30451  bnj90  31089  bnj919  31136  bnj535  31259  bnj1463  31422  frrlem1  32078  fnchoice  39679
  Copyright terms: Public domain W3C validator