![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > funeqi | Structured version Visualization version GIF version |
Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
funeqi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
funeqi | ⊢ (Fun 𝐴 ↔ Fun 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funeqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | funeq 6245 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (Fun 𝐴 ↔ Fun 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ 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: funmpt 6263 funmpt2 6264 funco 6265 funresfunco 6266 fununfun 6272 funprg 6278 funtpg 6279 funtp 6281 funcnvpr 6286 funcnvtp 6287 funcnvqp 6288 funcnv0 6290 f1cnvcnv 6452 f1co 6453 opabiotafun 6611 fvn0ssdmfun 6707 funopdmsn 6775 fpropnf1 6890 funoprabg 7129 mpofun 7132 ovidig 7148 funcnvuni 7492 fiun 7500 f1iun 7501 tposfun 7759 tfr1a 7882 tz7.44lem1 7893 tz7.48-2 7929 ssdomg 8403 sbthlem7 8480 sbthlem8 8481 1sdom 8567 hartogslem1 8852 r1funlim 9041 zorn2lem4 9767 axaddf 10413 axmulf 10414 fundmge2nop0 13696 funcnvs1 14110 strleun 16420 fthoppc 17022 cnfldfun 20239 cnfldfunALT 20240 volf 23813 dfrelog 24830 usgredg3 26681 ushgredgedg 26694 ushgredgedgloop 26696 2trld 27404 0pth 27591 1pthdlem1 27601 1trld 27608 3trld 27638 ajfuni 28327 hlimf 28705 funadj 29354 funcnvadj 29361 rinvf1o 30065 bnj97 31754 bnj150 31764 bnj1384 31918 bnj1421 31928 bnj60 31948 satffunlem2lem2 32261 satfv0fvfmla0 32268 funpartfun 33013 funtransport 33101 funray 33210 funline 33212 xlimfun 41678 funcoressn 42793 |
Copyright terms: Public domain | W3C validator |