Theorem feq23d 6701

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 6695	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-fun 6533  df-fn 6534  df-f 6535

This theorem is referenced by:  nvof1o  7273  axdc4uz  14002  isacs  17663  isfunc  17877  funcres  17909  funcpropd  17915  estrcco  18142  funcestrcsetclem9  18160  fullestrcsetc  18163  fullsetcestrc  18178  1stfcl  18209  2ndfcl  18210  evlfcl  18234  curf1cl  18240  yonedalem3b  18291  intopsn  18632  mgmhmpropd  18676  mhmpropd  18770  isghm  19198  pwssplit1  21017  islindf  21772  evls1sca  22261  rrxds  25345  wlkp1  29661  acunirnmpt  32637  fnpreimac  32649  pwrssmgc  32980  cnmbfm  34295  elmrsubrn  35542  poimirlem3  37647  poimirlem28  37672  isrngod  37922  rngosn3  37948  isgrpda  37979  islfld  39080  tendofset  40777  tendoset  40778  sn-isghm  42696  mapfzcons  42739  diophrw  42782  refsum2cnlem1  45061  funcringcsetcALTV2lem9  48273  funcringcsetclem9ALTV  48296  termcfuncval  49417  aacllem  49665