Theorem feq23d 6595

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-fun 6435  df-fn 6436  df-f 6437

This theorem is referenced by:  nvof1o  7152  axdc4uz  13704  isacs  17360  isfunc  17579  funcres  17611  funcpropd  17616  estrcco  17846  funcestrcsetclem9  17865  fullestrcsetc  17868  fullsetcestrc  17883  1stfcl  17914  2ndfcl  17915  evlfcl  17940  curf1cl  17946  yonedalem3b  17997  intopsn  18338  mhmpropd  18436  pwssplit1  20321  islindf  21019  evls1sca  21489  rrxds  24557  wlkp1  28049  acunirnmpt  30996  fnpreimac  31008  pwrssmgc  31278  cnmbfm  32230  elmrsubrn  33482  poimirlem3  35780  poimirlem28  35805  isrngod  36056  rngosn3  36082  isgrpda  36113  islfld  37076  tendofset  38772  tendoset  38773  mapfzcons  40538  diophrw  40581  refsum2cnlem1  42580  mgmhmpropd  45339  funcringcsetcALTV2lem9  45602  funcringcsetclem9ALTV  45625  aacllem  46505