Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
The Predecessor Class
cpred

Next ⟩ df-pred

Metamath Proof Explorer

Unicode
Structured

Syntax definition cpred

Description: The predecessors symbol.

		Ref	Expression
	Assertion	cpred	class Pred ( R , A , X )