![]() |
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 6245 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1522 Fun wfun 6219 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-in 3866 df-ss 3874 df-br 4963 df-opab 5025 df-rel 5450 df-cnv 5451 df-co 5452 df-fun 6227 |
This theorem is referenced by: funopg 6259 funsng 6275 f1eq1 6438 f1ssf1 6514 fvn0ssdmfun 6707 funcnvuni 7492 fundmge2nop0 13696 funcnvs2 14111 funcnvs3 14112 funcnvs4 14113 shftfn 14266 isstruct2 16322 structfung 16327 setsfun 16347 setsfun0 16348 strle1 16421 monfval 16831 ismon 16832 monpropd 16836 isepi 16839 isfth 17013 estrres 17218 lubfun 17419 glbfun 17432 acsficl2d 17615 frlmphl 20607 ebtwntg 26451 ecgrtg 26452 elntg 26453 uhgrspansubgrlem 26755 istrl 27163 ispth 27191 isspth 27192 upgrwlkdvspth 27207 uhgrwkspthlem1 27221 uhgrwkspthlem2 27222 usgr2wlkspthlem1 27225 usgr2wlkspthlem2 27226 pthdlem1 27234 2spthd 27407 0spth 27592 3spthd 27642 trlsegvdeglem2 27688 trlsegvdeglem3 27689 ajfun 28328 fresf1o 30066 padct 30143 smatrcl 30676 esum2dlem 30968 omssubadd 31175 sitgf 31222 funen1cnv 31971 pthhashvtx 31982 satfv0fun 32226 satffunlem1 32262 satffunlem2 32263 satffun 32264 satefvfmla0 32273 satefvfmla1 32280 fperdvper 41744 ovnovollem1 42480 funressnmo 42797 dfateq12d 42841 afvres 42887 funressndmafv2rn 42938 afv2res 42954 fdivval 44080 |
Copyright terms: Public domain | W3C validator |