| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > funeqd | Structured version Visualization version GIF version | ||
| Description: Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
| Ref | Expression |
|---|---|
| funeqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| funeqd | ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funeqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | funeq 6586 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 Fun wfun 6555 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 df-br 5144 df-opab 5206 df-rel 5692 df-cnv 5693 df-co 5694 df-fun 6563 |
| This theorem is referenced by: funopg 6600 funsng 6617 f1eq1 6799 f1ssf1 6880 fvn0ssdmfun 7094 funcnvuni 7954 fundmge2nop0 14541 funcnvs2 14952 funcnvs3 14953 funcnvs4 14954 shftfn 15112 isstruct2 17186 structfung 17191 strle1 17195 setsfun 17208 setsfun0 17209 monfval 17776 ismon 17777 monpropd 17781 isepi 17784 isfth 17961 estrres 18184 lubfun 18397 glbfun 18410 acsficl2d 18597 ebtwntg 28997 ecgrtg 28998 elntg 28999 uhgrspansubgrlem 29307 istrl 29714 ispth 29741 isspth 29742 dfpth2 29749 upgrwlkdvspth 29759 uhgrwkspthlem1 29773 uhgrwkspthlem2 29774 usgr2wlkspthlem1 29777 usgr2wlkspthlem2 29778 pthdlem1 29786 2spthd 29961 0spth 30145 3spthd 30195 trlsegvdeglem2 30240 trlsegvdeglem3 30241 ajfun 30879 fresf1o 32641 padct 32731 smatrcl 33795 esum2dlem 34093 omssubadd 34302 sitgf 34349 funen1cnv 35102 pthhashvtx 35133 satfv0fun 35376 satffunlem1 35412 satffunlem2 35413 satffun 35414 satefvfmla0 35423 satefvfmla1 35430 fperdvper 45934 ovnovollem1 46671 funressnmo 47058 dfateq12d 47138 afvres 47184 funressndmafv2rn 47235 afv2res 47251 fdivval 48460 |
| Copyright terms: Public domain | W3C validator |