Theorem feq23d 6696

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  nvof1o  7280  axdc4uz  14107  isacs  17805  isfunc  18019  funcres  18051  funcpropd  18057  estrcco  18284  funcestrcsetclem9  18302  fullestrcsetc  18305  fullsetcestrc  18320  1stfcl  18351  2ndfcl  18352  evlfcl  18376  curf1cl  18382  yonedalem3b  18433  intopsn  18812  mgmhmpropd  18867  mhmpropd  18967  isghm  19410  pwssplit1  21314  islindf  22098  evls1sca  22621  rrxds  25694  wlkp1  30242  acunirnmpt  33235  fnpreimac  33246  pwrssmgc  33543  cnmbfm  34878  elmrsubrn  36254  poimirlem3  38509  poimirlem28  38534  isrngod  38800  rngosn3  38826  isgrpda  38857  islfld  40087  tendofset  41783  tendoset  41784  sn-isghm  43638  mapfzcons  43680  diophrw  43723  refsum2cnlem1  45997  funcringcsetcALTV2lem9  49339  funcringcsetclem9ALTV  49362  termcfuncval  50584  aacllem  50883