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 5823 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (Fun 𝐴 ↔ Fun 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 Fun wfun 5798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-in 3547 df-ss 3554 df-br 4584 df-opab 4644 df-rel 5045 df-cnv 5046 df-co 5047 df-fun 5806 |
This theorem is referenced by: funmpt 5840 funmpt2 5841 funco 5842 fununfun 5848 funprg 5854 funprgOLD 5855 funtpg 5856 funtpgOLD 5857 funtp 5859 funcnvpr 5864 funcnvtp 5865 funcnvqp 5866 funcnvqpOLD 5867 funcnv0 5869 f1cnvcnv 6022 f1co 6023 f10 6081 opabiotafun 6169 fvn0ssdmfun 6258 funoprabg 6657 mpt2fun 6660 ovidig 6676 funcnvuni 7012 fun11iun 7019 tposfun 7255 tfr1a 7377 tz7.44lem1 7388 tz7.48-2 7424 ssdomg 7887 sbthlem7 7961 sbthlem8 7962 1sdom 8048 hartogslem1 8330 r1funlim 8512 zorn2lem4 9204 axaddf 9845 axmulf 9846 fundmge2nop0 13129 funcnvs1 13507 structfun 15707 strlemor1 15796 strleun 15799 fthoppc 16406 volf 23104 dfrelog 24116 0pth 26100 1pthonlem1 26119 2pthlem1 26125 ajfuni 27099 hlimf 27478 funadj 28129 funcnvadj 28136 rinvf1o 28814 funcnvmptOLD 28850 bnj97 30190 bnj150 30200 bnj1384 30354 bnj1421 30364 bnj60 30384 frrlem10 31035 funpartfun 31220 funtransport 31308 funray 31417 funline 31419 funresfunco 39854 funcoressn 39856 fpropnf1 40337 uhgr2edg 40435 usgredg3 40443 ushgredgedga 40456 ushgredgedgaloop 40458 2trld 41145 0pth-av 41293 1pthdlem1 41302 1trld 41309 3trld 41339 |
Copyright terms: Public domain | W3C validator |