![]() |
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 6578 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (Fun 𝐴 ↔ Fun 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 Fun wfun 6547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ss 3963 df-br 5153 df-opab 5215 df-rel 5688 df-cnv 5689 df-co 5690 df-fun 6555 |
This theorem is referenced by: funopg 6592 funsng 6609 f1eq1 6792 f1ssf1 6874 fvn0ssdmfun 7087 funcnvuni 7944 fundmge2nop0 14506 funcnvs2 14917 funcnvs3 14918 funcnvs4 14919 shftfn 15073 isstruct2 17146 structfung 17151 strle1 17155 setsfun 17168 setsfun0 17169 monfval 17743 ismon 17744 monpropd 17748 isepi 17751 isfth 17931 estrres 18158 lubfun 18372 glbfun 18385 acsficl2d 18572 ebtwntg 28908 ecgrtg 28909 elntg 28910 uhgrspansubgrlem 29218 istrl 29625 ispth 29652 isspth 29653 upgrwlkdvspth 29668 uhgrwkspthlem1 29682 uhgrwkspthlem2 29683 usgr2wlkspthlem1 29686 usgr2wlkspthlem2 29687 pthdlem1 29695 2spthd 29867 0spth 30051 3spthd 30101 trlsegvdeglem2 30146 trlsegvdeglem3 30147 ajfun 30785 fresf1o 32539 padct 32624 smatrcl 33567 esum2dlem 33881 omssubadd 34090 sitgf 34137 funen1cnv 34881 pthhashvtx 34907 satfv0fun 35151 satffunlem1 35187 satffunlem2 35188 satffun 35189 satefvfmla0 35198 satefvfmla1 35205 fperdvper 45477 ovnovollem1 46214 funressnmo 46598 dfateq12d 46676 afvres 46722 funressndmafv2rn 46773 afv2res 46789 fdivval 47864 |
Copyright terms: Public domain | W3C validator |