Theorem feq23d 6686

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  nvof1o  7258  axdc4uz  13956  isacs  17619  isfunc  17833  funcres  17865  funcpropd  17871  estrcco  18098  funcestrcsetclem9  18116  fullestrcsetc  18119  fullsetcestrc  18134  1stfcl  18165  2ndfcl  18166  evlfcl  18190  curf1cl  18196  yonedalem3b  18247  intopsn  18588  mgmhmpropd  18632  mhmpropd  18726  isghm  19154  pwssplit1  20973  islindf  21728  evls1sca  22217  rrxds  25300  wlkp1  29616  acunirnmpt  32590  fnpreimac  32602  pwrssmgc  32933  cnmbfm  34261  elmrsubrn  35514  poimirlem3  37624  poimirlem28  37649  isrngod  37899  rngosn3  37925  isgrpda  37956  islfld  39062  tendofset  40759  tendoset  40760  sn-isghm  42668  mapfzcons  42711  diophrw  42754  refsum2cnlem1  45038  funcringcsetcALTV2lem9  48290  funcringcsetclem9ALTV  48313  termcfuncval  49525  aacllem  49794