ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fneq2 GIF version

Theorem fneq2 5261
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 2167 . . 3 (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵))
21anbi2d 460 . 2 (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)))
3 df-fn 5175 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
4 df-fn 5175 . 2 (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
52, 3, 43bitr4g 222 1 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1335  dom cdm 4588  Fun wfun 5166   Fn wfn 5167
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-fn 5175
This theorem is referenced by:  fneq2d  5263  fneq2i  5267  feq2  5305  foeq2  5391  f1o00  5451  eqfnfv2  5568  tfr0dm  6271  tfrlemisucaccv  6274  tfrlemi1  6281  tfrlemi14d  6282  tfrexlem  6283  tfr1onlemsucfn  6289  tfr1onlemsucaccv  6290  tfr1onlembxssdm  6292  tfr1onlembfn  6293  tfr1onlemaccex  6297  tfr1onlemres  6298  ixpeq1  6656  0fz1  9953
  Copyright terms: Public domain W3C validator