Theorem fneq2 6598

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1550  dom cdm 5636  Fun wfun 6500   Fn wfn 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744  df-fn 6509

This theorem is referenced by:  fneq2d  6600  fneq2i  6604  feq2  6655  foeq2  6760  f1o00  6827  eqfnfv2  6997  frrlem1  8251  frrlem13  8263  tfrlem12  8344  ixpeq1  8875  ac5  10420  0fz1  13535  fconst7v  32761  esumcvgsum  34329  bnj90  34965  bnj919  35010  bnj535  35132  bnj1463  35297  fnchoice  45547