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

Theorem fneq2 5948
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 2632 . . 3 (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵))
21anbi2d 739 . 2 (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)))
3 df-fn 5860 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
4 df-fn 5860 . 2 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
52, 3, 43bitr4g 303 1 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  dom cdm 5084  Fun wfun 5851   Fn wfn 5852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-fn 5860
This theorem is referenced by:  fneq2d  5950  fneq2i  5954  feq2  5994  foeq2  6079  f1o00  6138  eqfnfv2  6278  wfrlem1  7374  wfrlem15  7389  tfrlem12  7445  ixpeq1  7879  ac5  9259  0fz1  12319  esumcvgsum  29973  bnj90  30549  bnj919  30598  bnj535  30721  bnj1463  30884  frrlem1  31534  fnchoice  38710
  Copyright terms: Public domain W3C validator