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 6492 | . 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐴⟶𝐶)) |
3 | feq12d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | feq2d 6493 | . 2 ⊢ (𝜑 → (𝐺:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
5 | 2, 4 | bitrd 280 | 1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ⟶wf 6344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-fun 6350 df-fn 6351 df-f 6352 |
This theorem is referenced by: feq123d 6496 fprg 6909 smoeq 7976 oif 8982 1fv 13014 catcisolem 17354 hofcl 17497 dmdprd 19049 dpjf 19108 pjf2 20786 mat1dimmul 21013 lmbr2 21795 lmff 21837 dfac14 22154 lmmbr2 23789 lmcau 23843 perfdvf 24428 dvnfre 24476 dvle 24531 dvfsumle 24545 dvfsumge 24546 dvmptrecl 24548 uhgr0e 26783 uhgrstrrepe 26790 incistruhgr 26791 upgr1e 26825 1hevtxdg1 27215 umgr2v2e 27234 iswlk 27319 0wlkons1 27827 resf1o 30392 ismeas 31357 omsmeas 31480 breprexplema 31800 satfun 32555 mbfresfi 34819 sdclem1 34899 dfac21 39544 fnlimfvre 41831 climrescn 41905 fourierdlem74 42342 fourierdlem103 42371 fourierdlem104 42372 sge0iunmpt 42577 ismea 42610 isome 42653 sssmf 42892 smflimlem3 42926 smflimlem4 42927 isupwlk 43888 |
Copyright terms: Public domain | W3C validator |