Theorem feq2i 5527

Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.)

Hypothesis

Ref	Expression
feq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
feq2i	⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)

Proof of Theorem feq2i

Step	Hyp	Ref	Expression
1		feq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		feq2 5517	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402  ⟶wf 5373

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  df-f 5381

This theorem is used by:  fmpox  6436  fmpo  6437  tposf  6543  issmo  6559  tfrcllemsucfn  6624  1fv  10548  fxnn0nninf  10878  snopiswrd  11316  iswrddm0  11330  gsum0cmn  14156  0met  15487  dvef  15830  uhgr0e  16335  vtxdumgrfival  16551