![]() |
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 6576 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (Fun 𝐴 ↔ Fun 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 Fun wfun 6545 |
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 2698 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3473 df-in 3954 df-ss 3964 df-br 5151 df-opab 5213 df-rel 5687 df-cnv 5688 df-co 5689 df-fun 6553 |
This theorem is referenced by: funmpt 6594 funmpt2 6595 funco 6596 funresfunco 6597 fununfun 6604 funprg 6610 funtpg 6611 funtp 6613 funcnvpr 6618 funcnvtp 6619 funcnvqp 6620 funcnv0 6622 f1cnvcnv 6806 f1cof1 6807 f1coOLD 6809 opabiotafun 6982 fvn0ssdmfun 7087 funopdmsn 7163 fpropnf1 7281 funoprabg 7545 mpofun 7548 mpofunOLD 7549 ovidig 7567 funcnvuni 7943 fiun 7950 f1iun 7951 tposfun 8252 tfr1a 8419 tz7.44lem1 8430 tz7.48-2 8467 ssdomg 9025 sbthlem7 9118 sbthlem8 9119 1sdomOLD 9278 hartogslem1 9571 r1funlim 9795 zorn2lem4 10528 axaddf 11174 axmulf 11175 fundmge2nop0 14491 funcnvs1 14901 strleun 17131 fthoppc 17917 cnfldfun 21298 cnfldfunALT 21299 cnfldfunOLD 21311 cnfldfunALTOLD 21312 cnfldfunALTOLDOLD 21313 volf 25476 dfrelog 26517 precsexlem10 28132 precsexlem11 28133 usgredg3 29047 ushgredgedg 29060 ushgredgedgloop 29062 2trld 29767 0pth 29953 1pthdlem1 29963 1trld 29970 3trld 30000 ajfuni 30687 hlimf 31065 funadj 31714 funcnvadj 31721 rinvf1o 32433 bnj97 34502 bnj150 34512 bnj1384 34668 bnj1421 34678 bnj60 34698 satffunlem2lem2 35021 satfv0fvfmla0 35028 funpartfun 35544 funtransport 35632 funray 35741 funline 35743 xlimfun 45245 funcoressn 46426 |
Copyright terms: Public domain | W3C validator |