Theorem feq23d 6683

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  nvof1o  7255  axdc4uz  13949  isacs  17612  isfunc  17826  funcres  17858  funcpropd  17864  estrcco  18091  funcestrcsetclem9  18109  fullestrcsetc  18112  fullsetcestrc  18127  1stfcl  18158  2ndfcl  18159  evlfcl  18183  curf1cl  18189  yonedalem3b  18240  intopsn  18581  mgmhmpropd  18625  mhmpropd  18719  isghm  19147  pwssplit1  20966  islindf  21721  evls1sca  22210  rrxds  25293  wlkp1  29609  acunirnmpt  32583  fnpreimac  32595  pwrssmgc  32926  cnmbfm  34254  elmrsubrn  35507  poimirlem3  37617  poimirlem28  37642  isrngod  37892  rngosn3  37918  isgrpda  37949  islfld  39055  tendofset  40752  tendoset  40753  sn-isghm  42661  mapfzcons  42704  diophrw  42747  refsum2cnlem1  45031  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  termcfuncval  49521  aacllem  49790