Theorem feq23d 6732

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ⟶wf 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-fun 6565  df-fn 6566  df-f 6567

This theorem is referenced by:  nvof1o  7300  axdc4uz  14022  isacs  17696  isfunc  17915  funcres  17947  funcpropd  17954  estrcco  18185  funcestrcsetclem9  18204  fullestrcsetc  18207  fullsetcestrc  18222  1stfcl  18253  2ndfcl  18254  evlfcl  18279  curf1cl  18285  yonedalem3b  18336  intopsn  18680  mgmhmpropd  18724  mhmpropd  18818  isghm  19246  pwssplit1  21076  islindf  21850  evls1sca  22343  rrxds  25441  wlkp1  29714  acunirnmpt  32676  fnpreimac  32688  pwrssmgc  32975  cnmbfm  34245  elmrsubrn  35505  poimirlem3  37610  poimirlem28  37635  isrngod  37885  rngosn3  37911  isgrpda  37942  islfld  39044  tendofset  40741  tendoset  40742  sn-isghm  42660  mapfzcons  42704  diophrw  42747  refsum2cnlem1  44975  funcringcsetcALTV2lem9  48142  funcringcsetclem9ALTV  48165  aacllem  49032