![]() |
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 6650 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐴⟶𝐶)) |
3 | feq12d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | feq2d 6651 | . 2 ⊢ (𝜑 → (𝐺:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
5 | 2, 4 | bitrd 278 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1541 ⟶wf 6489 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-fun 6495 df-fn 6496 df-f 6497 |
This theorem is referenced by: feq123d 6654 fprg 7097 smoeq 8292 oif 9462 1fv 13552 catcisolem 17988 hofcl 18140 dmdprd 19768 dpjf 19827 pjf2 21105 mat1dimmul 21809 lmbr2 22594 lmff 22636 dfac14 22953 lmmbr2 24607 lmcau 24661 perfdvf 25251 dvnfre 25300 dvle 25355 dvfsumle 25369 dvfsumge 25370 dvmptrecl 25372 uhgr0e 27908 uhgrstrrepe 27915 incistruhgr 27916 upgr1e 27950 1hevtxdg1 28340 umgr2v2e 28359 iswlk 28444 0wlkons1 28951 resf1o 31530 ismeas 32667 omsmeas 32792 breprexplema 33112 satfun 33874 mbfresfi 36091 sdclem1 36169 dfac21 41331 fnlimfvre 43847 climrescn 43921 fourierdlem74 44353 fourierdlem103 44382 fourierdlem104 44383 sge0iunmpt 44591 ismea 44624 isome 44667 sssmf 44911 smflimlem3 44946 smflimlem4 44947 isupwlk 45970 |
Copyright terms: Public domain | W3C validator |