Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > feq12d | Structured version Visualization version GIF version |
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
feq12d.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
feq12d.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
feq12d | ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq12d.1 | . . 3 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | 1 | feq1d 6569 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐴⟶𝐶)) |
3 | feq12d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | feq2d 6570 | . 2 ⊢ (𝜑 → (𝐺:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
5 | 2, 4 | bitrd 278 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1539 ⟶wf 6414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-br 5071 df-opab 5133 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-fun 6420 df-fn 6421 df-f 6422 |
This theorem is referenced by: feq123d 6573 fprg 7009 smoeq 8152 oif 9219 1fv 13304 catcisolem 17741 hofcl 17893 dmdprd 19516 dpjf 19575 pjf2 20831 mat1dimmul 21533 lmbr2 22318 lmff 22360 dfac14 22677 lmmbr2 24328 lmcau 24382 perfdvf 24972 dvnfre 25021 dvle 25076 dvfsumle 25090 dvfsumge 25091 dvmptrecl 25093 uhgr0e 27344 uhgrstrrepe 27351 incistruhgr 27352 upgr1e 27386 1hevtxdg1 27776 umgr2v2e 27795 iswlk 27880 0wlkons1 28386 resf1o 30967 ismeas 32067 omsmeas 32190 breprexplema 32510 satfun 33273 mbfresfi 35750 sdclem1 35828 dfac21 40807 fnlimfvre 43105 climrescn 43179 fourierdlem74 43611 fourierdlem103 43640 fourierdlem104 43641 sge0iunmpt 43846 ismea 43879 isome 43922 sssmf 44161 smflimlem3 44195 smflimlem4 44196 isupwlk 45186 |
Copyright terms: Public domain | W3C validator |