Theorem fneq2 6635

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  dom cdm 5659  Fun wfun 6530   Fn wfn 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-fn 6539

This theorem is referenced by:  fneq2d  6637  fneq2i  6641  feq2  6692  foeq2  6792  f1o00  6858  eqfnfv2  7027  frrlem1  8290  frrlem13  8302  wfrlem1OLD  8327  wfrlem15OLD  8342  tfrlem12  8408  ixpeq1  8927  ac5  10496  0fz1  13566  esumcvgsum  34124  bnj90  34758  bnj919  34803  bnj535  34926  bnj1463  35091  fnchoice  45020