Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Introduce the Axiom of Extensionality

Next ⟩ ax-ext

Metamath Proof Explorer

Ascii
Structured

Table of Contents - 2.1.1. Introduce the Axiom of Extensionality

ax-ext
axexte
axextg
axextb
axextmo
nulmo