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

Step	Hyp	Ref	Expression
1		eqeq2 2621	. . 3 ⊢ (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵))
2	1	anbi2d 736	. 2 ⊢ (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)))
3		df-fn 5807	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
4		df-fn 5807	. 2 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
5	2, 3, 4	3bitr4g 302	1 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))

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