Theorem fneq2 6671

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 2752	. . 3 ⊢ (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵))
2	1	anbi2d 629	. 2 ⊢ (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)))
3		df-fn 6576	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
4		df-fn 6576	. 2 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  dom cdm 5700  Fun wfun 6567   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576

This theorem is referenced by:  fneq2d  6673  fneq2i  6677  feq2  6729  foeq2  6831  f1o00  6897  eqfnfv2  7065  frrlem1  8327  frrlem13  8339  wfrlem1OLD  8364  wfrlem15OLD  8379  tfrlem12  8445  ixpeq1  8966  ac5  10546  0fz1  13604  esumcvgsum  34052  bnj90  34698  bnj919  34743  bnj535  34866  bnj1463  35031  fnchoice  44929