Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Define basic set operations and relations
wpss

Next ⟩ difjust

Metamath Proof Explorer

Ascii
Unicode

Syntax definition wpss

Description: Extend wff notation with proper subclass relation.

		Ref	Expression
	Assertion	wpss	$wff A \subset B$