Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Universal and existential quantifiers, nonfreeness predicate
Next ⟩
Adding ax-gen
Metamath Proof Explorer
Ascii
Unicode
Table of Contents - 21.20.4.1. Universal and existential quantifiers, nonfreeness predicate