Theorem feq23d 6482

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ⟶wf 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328

This theorem is referenced by:  nvof1o  7015  axdc4uz  13347  isacs  16914  isfunc  17126  funcres  17158  funcpropd  17162  estrcco  17372  funcestrcsetclem9  17390  fullestrcsetc  17393  fullsetcestrc  17408  1stfcl  17439  2ndfcl  17440  evlfcl  17464  curf1cl  17470  yonedalem3b  17521  intopsn  17856  mhmpropd  17954  pwssplit1  19824  islindf  20501  evls1sca  20947  rrxds  23997  wlkp1  27471  acunirnmpt  30422  fnpreimac  30434  pwrssmgc  30706  cnmbfm  31631  elmrsubrn  32880  poimirlem3  35060  poimirlem28  35085  isrngod  35336  rngosn3  35362  isgrpda  35393  islfld  36358  tendofset  38054  tendoset  38055  mapfzcons  39657  diophrw  39700  refsum2cnlem1  41666  mgmhmpropd  44405  funcringcsetcALTV2lem9  44668  funcringcsetclem9ALTV  44691  aacllem  45329