Theorem feq23d 6657

Description: Equality deduction for functions. (Contributed by NM, 8-Jun-2013.)

Hypotheses

Ref	Expression
feq23d.1	⊢ (𝜑 → 𝐴 = 𝐶)
feq23d.2	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
feq23d	⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))

Proof of Theorem feq23d

Step	Hyp	Ref	Expression
1		eqidd 2737	. 2 ⊢ (𝜑 → 𝐹 = 𝐹)
2		feq23d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
3		feq23d.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
4	1, 2, 3	feq123d 6651	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  nvof1o  7226  axdc4uz  13907  isacs  17574  isfunc  17788  funcres  17820  funcpropd  17826  estrcco  18053  funcestrcsetclem9  18071  fullestrcsetc  18074  fullsetcestrc  18089  1stfcl  18120  2ndfcl  18121  evlfcl  18145  curf1cl  18151  yonedalem3b  18202  intopsn  18579  mgmhmpropd  18623  mhmpropd  18717  isghm  19144  pwssplit1  21011  islindf  21767  evls1sca  22267  rrxds  25349  wlkp1  29753  acunirnmpt  32737  fnpreimac  32749  pwrssmgc  33082  cnmbfm  34420  elmrsubrn  35714  poimirlem3  37824  poimirlem28  37849  isrngod  38099  rngosn3  38125  isgrpda  38156  islfld  39322  tendofset  41018  tendoset  41019  sn-isghm  42916  mapfzcons  42958  diophrw  43001  refsum2cnlem1  45282  funcringcsetcALTV2lem9  48544  funcringcsetclem9ALTV  48567  termcfuncval  49777  aacllem  50046