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

Metamath Proof Explorer

Theorem sucprcreg

Description: A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004) (Proof shortened by BJ, 16-Apr-2019)

		Ref	Expression
	Assertion	sucprcreg	$⊢ \neg A \in V \leftrightarrow suc A = A$

Proof

Step	Hyp	Ref	Expression
1		sucprc	$⊢ \neg A \in V \to suc A = A$
2		elirr	$⊢ \neg A \in A$
3		df-suc	$⊢ suc A = A \cup \{A\}$
4	3	eqeq1i	$⊢ suc A = A \leftrightarrow A \cup \{A\} = A$
5		ssequn2	$⊢ \{A\} \subseteq A \leftrightarrow A \cup \{A\} = A$
6	4 5	sylbb2	$⊢ suc A = A \to \{A\} \subseteq A$
7		snidg	$⊢ A \in V \to A \in \{A\}$
8		ssel2	$⊢ (\{A\} \subseteq A \land A \in \{A\}) \to A \in A$
9	6 7 8	syl2an	$⊢ (suc A = A \land A \in V) \to A \in A$
10	2 9	mto	$⊢ \neg (suc A = A \land A \in V)$
11	10	imnani	$⊢ suc A = A \to \neg A \in V$
12	1 11	impbii	$⊢ \neg A \in V \leftrightarrow suc A = A$