| 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 6586 | . 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (Fun 𝐴 ↔ Fun 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 Fun wfun 6555 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ss 3968 df-br 5144 df-opab 5206 df-rel 5692 df-cnv 5693 df-co 5694 df-fun 6563 |
| This theorem is referenced by: funmpt 6604 funmpt2 6605 funco 6606 funresfunco 6607 fununfun 6614 funprg 6620 funtpg 6621 funtp 6623 funcnvpr 6628 funcnvtp 6629 funcnvqp 6630 funcnv0 6632 f1cnvcnv 6813 f1cof1 6814 opabiotafun 6989 fvn0ssdmfun 7094 funopdmsn 7170 fpropnf1 7287 funoprabg 7554 mpofun 7557 ovidig 7575 funcnvuni 7954 resf1extb 7956 fiun 7967 f1iun 7968 tposfun 8267 tfr1a 8434 tz7.44lem1 8445 tz7.48-2 8482 ssdomg 9040 sbthlem7 9129 sbthlem8 9130 1sdomOLD 9285 hartogslem1 9582 r1funlim 9806 zorn2lem4 10539 axaddf 11185 axmulf 11186 fundmge2nop0 14541 funcnvs1 14951 strleun 17194 fthoppc 17970 cnfldfun 21378 cnfldfunALT 21379 cnfldfunOLD 21391 cnfldfunALTOLD 21392 cnfldfunALTOLDOLD 21393 volf 25564 dfrelog 26607 precsexlem10 28240 precsexlem11 28241 usgredg3 29233 ushgredgedg 29246 ushgredgedgloop 29248 2trld 29958 0pth 30144 1pthdlem1 30154 1trld 30161 3trld 30191 ajfuni 30878 hlimf 31256 funadj 31905 funcnvadj 31912 rinvf1o 32640 isconstr 33777 bnj97 34880 bnj150 34890 bnj1384 35046 bnj1421 35056 bnj60 35076 satffunlem2lem2 35411 satfv0fvfmla0 35418 funpartfun 35944 funtransport 36032 funray 36141 funline 36143 modelaxreplem2 44996 xlimfun 45870 funcoressn 47054 |
| Copyright terms: Public domain | W3C validator |