Theorem feq23d 6497

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

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

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-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-br 5036  df-opab 5098  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-fun 6341  df-fn 6342  df-f 6343

This theorem is referenced by:  nvof1o  7034  axdc4uz  13406  isacs  16985  isfunc  17198  funcres  17230  funcpropd  17234  estrcco  17451  funcestrcsetclem9  17469  fullestrcsetc  17472  fullsetcestrc  17487  1stfcl  17518  2ndfcl  17519  evlfcl  17543  curf1cl  17549  yonedalem3b  17600  intopsn  17935  mhmpropd  18033  pwssplit1  19904  islindf  20582  evls1sca  21047  rrxds  24098  wlkp1  27575  acunirnmpt  30524  fnpreimac  30536  pwrssmgc  30808  cnmbfm  31753  elmrsubrn  33002  poimirlem3  35366  poimirlem28  35391  isrngod  35642  rngosn3  35668  isgrpda  35699  islfld  36664  tendofset  38360  tendoset  38361  mapfzcons  40058  diophrw  40101  refsum2cnlem1  42067  mgmhmpropd  44800  funcringcsetcALTV2lem9  45063  funcringcsetclem9ALTV  45086  aacllem  45793