Metamath Proof Explorer
Table of Contents - 2.3.16. Functions
- wfun
- wfn
- wf
- wf1
- wfo
- wf1o
- cfv
- wiso
- df-fun
- df-fn
- df-f
- df-f1
- df-fo
- df-f1o
- df-fv
- df-isom
- dffun2
- dffun3
- dffun4
- dffun5
- dffun6f
- dffun6
- funmo
- funrel
- 0nelfun
- funss
- funeq
- funeqi
- funeqd
- nffun
- sbcfung
- funeu
- funeu2
- dffun7
- dffun8
- dffun9
- funfn
- funfnd
- funi
- nfunv
- funopg
- funopab
- funopabeq
- funopab4
- funmpt
- funmpt2
- funco
- funresfunco
- funres
- funresd
- funssres
- fun2ssres
- funun
- fununmo
- fununfun
- fundif
- funcnvsn
- funsng
- fnsng
- funsn
- funprg
- funtpg
- funpr
- funtp
- fnsn
- fnprg
- fntpg
- fntp
- funcnvpr
- funcnvtp
- funcnvqp
- fun0
- funcnv0
- funcnvcnv
- funcnv2
- funcnv
- funcnv3
- fun2cnv
- svrelfun
- fncnv
- fun11
- fununi
- funin
- funres11
- funcnvres
- cnvresid
- funcnvres2
- funimacnv
- funimass1
- funimass2
- imadif
- imain
- funimaexg
- funimaex
- isarep1
- isarep2
- fneq1
- fneq2
- fneq1d
- fneq2d
- fneq12d
- fneq12
- fneq1i
- fneq2i
- nffn
- fnfun
- fnfund
- fnrel
- fndm
- fndmi
- fndmd
- funfni
- fndmu
- fnbr
- fnop
- fneu
- fneu2
- fnun
- fnund
- fnunop
- fncofn
- fnco
- fncoOLD
- fnresdm
- fnresdisj
- 2elresin
- fnssresb
- fnssres
- fnssresd
- fnresin1
- fnresin2
- fnres
- idfn
- fnresi
- fnresiOLD
- fnima
- fn0
- fnimadisj
- fnimaeq0
- dfmpt3
- mptfnf
- fnmptf
- fnopabg
- fnopab
- mptfng
- fnmpt
- fnmptd
- mpt0
- fnmpti
- dmmpti
- dmmptd
- mptun
- partfun
- feq1
- feq2
- feq3
- feq23
- feq1d
- feq2d
- feq3d
- feq12d
- feq123d
- feq123
- feq1i
- feq2i
- feq12i
- feq23i
- feq23d
- nff
- sbcfng
- sbcfg
- elimf
- ffn
- ffnd
- dffn2
- ffun
- ffund
- frel
- freld
- frn
- frnd
- fdm
- fdmOLD
- fdmd
- fdmi
- dffn3
- ffrn
- ffrnb
- ffrnbd
- fss
- fssd
- fssdmd
- fssdm
- fimass
- fimacnv
- fcof
- fco
- fcoOLD
- fcod
- fco2
- fssxp
- funssxp
- ffdm
- ffdmd
- fdmrn
- funcofd
- fco3OLD
- opelf
- fun
- fun2
- fun2d
- fnfco
- fssres
- fssresd
- fssres2
- fresin
- resasplit
- fresaun
- fresaunres2
- fresaunres1
- fcoi1
- fcoi2
- feu
- fcnvres
- fimacnvdisj
- fint
- fin
- f0
- f00
- f0bi
- f0dom0
- f0rn0
- fconst
- fconstg
- fnconstg
- fconst6g
- fconst6
- f1eq1
- f1eq2
- f1eq3
- nff1
- dff12
- f1f
- f1fn
- f1fun
- f1rel
- f1dm
- f1dmOLD
- f1ss
- f1ssr
- f1ssres
- f1resf1
- f1cnvcnv
- f1cof1
- f1co
- f1coOLD
- foeq1
- foeq2
- foeq3
- nffo
- fof
- fofun
- fofn
- forn
- dffo2
- foima
- dffn4
- funforn
- fodmrnu
- fimadmfo
- fores
- fimadmfoALT
- focnvimacdmdm
- focofo
- foco
- foconst
- f1oeq1
- f1oeq2
- f1oeq3
- f1oeq23
- f1eq123d
- foeq123d
- f1oeq123d
- f1oeq1d
- f1oeq2d
- f1oeq3d
- nff1o
- f1of1
- f1of
- f1ofn
- f1ofun
- f1orel
- f1odm
- dff1o2
- dff1o3
- f1ofo
- dff1o4
- dff1o5
- f1orn
- f1f1orn
- f1ocnv
- f1ocnvb
- f1ores
- f1orescnv
- f1imacnv
- foimacnv
- foun
- f1oun
- resdif
- resin
- f1oco
- f1cnv
- funcocnv2
- fococnv2
- f1ococnv2
- f1cocnv2
- f1ococnv1
- f1cocnv1
- funcoeqres
- f1ssf1
- f10
- f10d
- f1o00
- fo00
- f1o0
- f1oi
- f1ovi
- f1osn
- f1osng
- f1sng
- fsnd
- f1oprswap
- f1oprg
- tz6.12-2
- fveu
- brprcneu
- fvprc
- fvprcALT
- rnfvprc
- fv2
- dffv3
- dffv4
- elfv
- fveq1
- fveq2
- fveq1i
- fveq1d
- fveq2i
- fveq2d
- 2fveq3
- fveq12i
- fveq12d
- fveqeq2d
- fveqeq2
- nffv
- nffvmpt1
- nffvd
- fvex
- fvexi
- fvexd
- fvif
- iffv
- fv3
- fvres
- fvresd
- funssfv
- tz6.12-1
- tz6.12
- tz6.12f
- tz6.12c
- tz6.12i
- fvbr0
- fvrn0
- fvssunirn
- ndmfv
- ndmfvrcl
- elfvdm
- elfvex
- elfvexd
- eliman0
- nfvres
- nfunsn
- fvfundmfvn0
- 0fv
- fv2prc
- elfv2ex
- fveqres
- csbfv12
- csbfv2g
- csbfv
- funbrfv
- funopfv
- fnbrfvb
- fnopfvb
- funbrfvb
- funopfvb
- fnbrfvb2
- funbrfv2b
- dffn5
- fnrnfv
- fvelrnb
- foelrni
- dfimafn
- dfimafn2
- funimass4
- fvelima
- fvelimad
- feqmptd
- feqresmpt
- feqmptdf
- dffn5f
- fvelimab
- fvelimabd
- unima
- fvi
- fviss
- fniinfv
- fnsnfv
- fnsnfvOLD
- opabiotafun
- opabiotadm
- opabiota
- fnimapr
- ssimaex
- ssimaexg
- funfv
- funfv2
- funfv2f
- fvun
- fvun1
- fvun2
- fvun1d
- fvun2d
- dffv2
- dmfco
- fvco2
- fvco
- fvco3
- fvco3d
- fvco4i
- fvopab3g
- fvopab3ig
- brfvopabrbr
- fvmptg
- fvmpti
- fvmpt
- fvmpt2f
- fvtresfn
- fvmpts
- fvmpt3
- fvmpt3i
- fvmptdf
- fvmptd
- fvmptd2
- mptrcl
- fvmpt2i
- fvmpt2
- fvmptss
- fvmpt2d
- fvmptex
- fvmptd3f
- fvmptd2f
- fvmptdv
- fvmptdv2
- mpteqb
- fvmptt
- fvmptf
- fvmptnf
- fvmptd3
- fvmptn
- fvmptss2
- elfvmptrab1w
- elfvmptrab1
- elfvmptrab
- fvopab4ndm
- fvmptndm
- fvmptrabfv
- fvopab5
- fvopab6
- eqfnfv
- eqfnfv2
- eqfnfv3
- eqfnfvd
- eqfnfv2f
- eqfunfv
- fvreseq0
- fvreseq1
- fvreseq
- fnmptfvd
- fndmdif
- fndmdifcom
- fndmdifeq0
- fndmin
- fneqeql
- fneqeql2
- fnreseql
- chfnrn
- funfvop
- funfvbrb
- fvimacnvi
- fvimacnv
- funimass3
- funimass5
- funconstss
- fvimacnvALT
- elpreima
- elpreimad
- fniniseg
- fncnvima2
- fniniseg2
- unpreima
- inpreima
- difpreima
- respreima
- cnvimainrn
- sspreima
- iinpreima
- intpreima
- fimacnvOLD
- fimacnvinrn
- fimacnvinrn2
- rescnvimafod
- fvn0ssdmfun
- fnopfv
- fvelrn
- nelrnfvne
- fveqdmss
- fveqressseq
- fnfvelrn
- ffvelrn
- ffvelrni
- ffvelrnda
- ffvelrnd
- rexrn
- ralrn
- elrnrexdm
- elrnrexdmb
- eldmrexrn
- eldmrexrnb
- fvcofneq
- ralrnmptw
- rexrnmptw
- ralrnmpt
- rexrnmpt
- f0cli
- dff2
- dff3
- dff4
- dffo3
- dffo4
- dffo5
- exfo
- foelrn
- foco2
- fmpt
- f1ompt
- fmpti
- fvmptelrn
- fmptd
- fmpttd
- fmpt3d
- fmptdf
- ffnfv
- ffnfvf
- fnfvrnss
- frnssb
- rnmptss
- fmpt2d
- ffvresb
- f1oresrab
- f1ossf1o
- fmptco
- fmptcof
- fmptcos
- cofmpt
- fcompt
- fcoconst
- fsn
- fsn2
- fsng
- fsn2g
- xpsng
- xpprsng
- xpsn
- f1o2sn
- residpr
- dfmpt
- fnasrn
- idref
- funiun
- funopsn
- funop
- funopdmsn
- funsndifnop
- funsneqopb
- ressnop0
- fpr
- fprg
- ftpg
- ftp
- fnressn
- funressn
- fressnfv
- fvrnressn
- fvressn
- fvn0fvelrn
- fvconst
- fnsnr
- fnsnb
- fmptsn
- fmptsng
- fmptsnd
- fmptap
- fmptapd
- fmptpr
- fvresi
- fninfp
- fnelfp
- fndifnfp
- fnelnfp
- fnnfpeq0
- fvunsn
- fvsng
- fvsn
- fvsnun1
- fvsnun2
- fnsnsplit
- fsnunf
- fsnunf2
- fsnunfv
- fsnunres
- funresdfunsn
- fvpr1
- fvpr2
- fvpr1g
- fvpr2g
- fprb
- fvtp1
- fvtp2
- fvtp3
- fvtp1g
- fvtp2g
- fvtp3g
- tpres
- fvconst2g
- fconst2g
- fvconst2
- fconst2
- fconst5
- rnmptc
- rnmptcOLD
- fnprb
- fntpb
- fnpr2g
- fpr2g
- fconstfv
- fconst3
- fconst4
- resfunexg
- resiexd
- fnex
- fnexd
- funex
- opabex
- mptexg
- mptexgf
- mptex
- mptexd
- mptrabex
- fex
- fexd
- mptfvmpt
- eufnfv
- funfvima
- funfvima2
- funfvima2d
- fnfvima
- fnfvimad
- resfvresima
- funfvima3
- rexima
- ralima
- fvclss
- elabrex
- abrexco
- imaiun
- imauni
- fniunfv
- funiunfv
- funiunfvf
- eluniima
- elunirn
- elunirnALT
- fnunirn
- dff13
- dff13f
- f1veqaeq
- f1cofveqaeq
- f1cofveqaeqALT
- 2f1fvneq
- f1mpt
- f1fveq
- f1elima
- f1imass
- f1imaeq
- f1imapss
- fpropnf1
- f1dom3fv3dif
- f1dom3el3dif
- dff14a
- dff14b
- f12dfv
- f13dfv
- dff1o6
- f1ocnvfv1
- f1ocnvfv2
- f1ocnvfv
- f1ocnvfvb
- nvof1o
- nvocnv
- fsnex
- f1prex
- f1ocnvdm
- f1ocnvfvrneq
- fcof1
- fcofo
- cbvfo
- cbvexfo
- cocan1
- cocan2
- fcof1oinvd
- fcof1od
- 2fcoidinvd
- fcof1o
- 2fvcoidd
- 2fvidf1od
- 2fvidinvd
- foeqcnvco
- f1eqcocnv
- f1eqcocnvOLD
- fveqf1o
- nf1const
- nf1oconst
- f1ofvswap
- fliftrel
- fliftel
- fliftel1
- fliftcnv
- fliftfun
- fliftfund
- fliftfuns
- fliftf
- fliftval
- isoeq1
- isoeq2
- isoeq3
- isoeq4
- isoeq5
- nfiso
- isof1o
- isof1oidb
- isof1oopb
- isorel
- soisores
- soisoi
- isoid
- isocnv
- isocnv2
- isocnv3
- isores2
- isores1
- isores3
- isotr
- isomin
- isoini
- isoini2
- isofrlem
- isoselem
- isofr
- isose
- isofr2
- isopolem
- isopo
- isosolem
- isoso
- isowe
- isowe2
- f1oiso
- f1oiso2
- f1owe
- weniso
- weisoeq
- weisoeq2
- knatar