Metamath Proof Explorer
Table of Contents - 20.43.1.6. Functions - extension
- fveqvfvv
- fnresfnco
- funcoressn
- funressnfv
- funressndmfvrn
- funressnvmo
- funressnmo
- funressneu
- fresfo
- fsetsniunop
- fsetabsnop
- fsetsnf
- fsetsnf1
- fsetsnfo
- fsetsnf1o
- fsetsnprcnex
- cfsetssfset
- cfsetsnfsetfv
- cfsetsnfsetf
- cfsetsnfsetf1
- cfsetsnfsetfo
- cfsetsnfsetf1o
- fsetprcnexALT
- fcoreslem1
- fcoreslem2
- fcoreslem3
- fcoreslem4
- fcores
- fcoresf1lem
- fcoresf1
- fcoresf1b
- fcoresfo
- fcoresfob
- fcoresf1ob
- f1cof1blem
- f1cof1b
- funfocofob
- fnfocofob
- focofob
- f1ocof1ob
- f1ocof1ob2