This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sucprc

Description: A proper class is its own successor. (Contributed by NM, 3-Apr-1995)

		Ref	Expression
	Assertion	sucprc	$⊢ \neg A \in V \to suc A = A$

Step	Hyp	Ref	Expression
1		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
2	1	biimpi	$⊢ \neg A \in V \to \{A\} = \emptyset$
3	2	uneq2d	$⊢ \neg A \in V \to A \cup \{A\} = A \cup \emptyset$
4		df-suc	$⊢ suc A = A \cup \{A\}$
5		un0	$⊢ A \cup \emptyset = A$
6	5	eqcomi	$⊢ A = A \cup \emptyset$
7	3 4 6	3eqtr4g	$⊢ \neg A \in V \to suc A = A$