Metamath Proof Explorer

Theorem class2seteq

Description: Writing a set as a class abstraction. This theorem looks artificial but was added to characterize the class abstraction whose existence is proved in class2set . (Contributed by NM, 13-Dec-2005) (Proof shortened by Raph Levien, 30-Jun-2006)

		Ref	Expression
	Assertion	class2seteq	$⊢ A \in V \to \{x \in A \| A \in V\} = A$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in V \to A \in V$
2		ax-1	$⊢ A \in V \to (x \in A \to A \in V)$
3	2	ralrimiv	$⊢ A \in V \to \forall x \in A A \in V$
4		rabid2	$⊢ A = \{x \in A \| A \in V\} \leftrightarrow \forall x \in A A \in V$
5	3 4	sylibr	$⊢ A \in V \to A = \{x \in A \| A \in V\}$
6	5	eqcomd	$⊢ A \in V \to \{x \in A \| A \in V\} = A$
7	1 6	syl	$⊢ A \in V \to \{x \in A \| A \in V\} = A$