Theorem feq23d 6646

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 2732	. 2 ⊢ (𝜑 → 𝐹 = 𝐹)
2		feq23d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
3		feq23d.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
4	1, 2, 3	feq123d 6640	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-fun 6483  df-fn 6484  df-f 6485

This theorem is referenced by:  nvof1o  7214  axdc4uz  13891  isacs  17557  isfunc  17771  funcres  17803  funcpropd  17809  estrcco  18036  funcestrcsetclem9  18054  fullestrcsetc  18057  fullsetcestrc  18072  1stfcl  18103  2ndfcl  18104  evlfcl  18128  curf1cl  18134  yonedalem3b  18185  intopsn  18562  mgmhmpropd  18606  mhmpropd  18700  isghm  19128  pwssplit1  20994  islindf  21750  evls1sca  22239  rrxds  25321  wlkp1  29659  acunirnmpt  32639  fnpreimac  32651  pwrssmgc  32979  cnmbfm  34274  elmrsubrn  35562  poimirlem3  37669  poimirlem28  37694  isrngod  37944  rngosn3  37970  isgrpda  38001  islfld  39107  tendofset  40803  tendoset  40804  sn-isghm  42712  mapfzcons  42755  diophrw  42798  refsum2cnlem1  45080  funcringcsetcALTV2lem9  48335  funcringcsetclem9ALTV  48358  termcfuncval  49570  aacllem  49839