Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Alternate definition of substitution

Next ⟩ bj-sbsb

Metamath Proof Explorer

Ascii
Unicode

Table of Contents - 21.20.4.21. Alternate definition of substitution

bj-sbsb
bj-dfsb2