![]() |
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 6241 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐴⟶𝐶)) |
3 | feq12d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | feq2d 6242 | . 2 ⊢ (𝜑 → (𝐺:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
5 | 2, 4 | bitrd 271 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1653 ⟶wf 6097 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-br 4844 df-opab 4906 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-fun 6103 df-fn 6104 df-f 6105 |
This theorem is referenced by: feq123d 6245 fprg 6650 smoeq 7686 oif 8677 1fv 12713 catcisolem 17070 hofcl 17214 dmdprd 18713 dpjf 18772 pjf2 20383 mat1dimmul 20608 lmbr2 21392 lmff 21434 dfac14 21750 lmmbr2 23385 lmcau 23439 perfdvf 24008 dvnfre 24056 dvle 24111 dvfsumle 24125 dvfsumge 24126 dvmptrecl 24128 uhgr0e 26306 uhgrstrrepe 26313 incistruhgr 26314 upgr1e 26348 1hevtxdg1 26756 umgr2v2e 26775 iswlk 26860 0wlkons1 27465 resf1o 30023 ismeas 30778 omsmeas 30901 breprexplema 31228 mbfresfi 33944 sdclem1 34026 dfac21 38421 fnlimfvre 40650 climrescn 40724 fourierdlem74 41140 fourierdlem103 41169 fourierdlem104 41170 sge0iunmpt 41378 ismea 41411 isome 41454 sssmf 41693 smflimlem3 41727 smflimlem4 41728 isupwlk 42516 |
Copyright terms: Public domain | W3C validator |