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

Theorem fneq2 6191
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 2817 . . 3 (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵))
21anbi2d 616 . 2 (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)))
3 df-fn 6104 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
4 df-fn 6104 . 2 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
52, 3, 43bitr4g 305 1 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  dom cdm 5311  Fun wfun 6095   Fn wfn 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-fn 6104
This theorem is referenced by:  fneq2d  6193  fneq2i  6197  feq2  6238  foeq2  6328  f1o00  6387  eqfnfv2  6534  wfrlem1  7649  wfrlem15  7665  tfrlem12  7721  ixpeq1  8156  ac5  9584  0fz1  12584  esumcvgsum  30475  bnj90  31113  bnj919  31160  bnj535  31283  bnj1463  31446  frrlem1  32101  fnchoice  39682
  Copyright terms: Public domain W3C validator