![]() |
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 6262 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐴⟶𝐶)) |
3 | feq12d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | feq2d 6263 | . 2 ⊢ (𝜑 → (𝐺:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
5 | 2, 4 | bitrd 271 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1658 ⟶wf 6118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-rab 3125 df-v 3415 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-br 4873 df-opab 4935 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-rn 5352 df-fun 6124 df-fn 6125 df-f 6126 |
This theorem is referenced by: feq123d 6266 fprg 6672 smoeq 7712 oif 8703 1fv 12752 catcisolem 17107 hofcl 17251 dmdprd 18750 dpjf 18809 pjf2 20420 mat1dimmul 20649 lmbr2 21433 lmff 21475 dfac14 21791 lmmbr2 23426 lmcau 23480 perfdvf 24065 dvnfre 24113 dvle 24168 dvfsumle 24182 dvfsumge 24183 dvmptrecl 24185 uhgr0e 26368 uhgrstrrepe 26375 incistruhgr 26376 upgr1e 26410 1hevtxdg1 26803 umgr2v2e 26822 iswlk 26907 0wlkons1 27496 resf1o 30052 ismeas 30806 omsmeas 30929 breprexplema 31256 mbfresfi 33998 sdclem1 34080 dfac21 38478 fnlimfvre 40700 climrescn 40774 fourierdlem74 41190 fourierdlem103 41219 fourierdlem104 41220 sge0iunmpt 41425 ismea 41458 isome 41501 sssmf 41740 smflimlem3 41774 smflimlem4 41775 isupwlk 42563 |
Copyright terms: Public domain | W3C validator |