Theorem fneq2d 5472

Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fneq2d	⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))

Proof of Theorem fneq2d

Step	Hyp	Ref	Expression
1		fneq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		fneq2 5470	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   Fn wfn 5372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5380

This theorem is used by:  fneq12d  5473  fncofn  5893  acfun  7564  ccfunen  7631  ccatlid  11389  ccatrid  11390  ccatass  11391  ccatswrd  11457  swrdccat2  11458  ccatpfx  11488  swrdswrd  11492  swrdccatin2  11516  pfxccatin12  11520  seq3shft  11618  ptex  13669  rng1zrlem  14309