Theorem class2seteq

Description: Equality theorem based on class2set . (Contributed by NM, 13-Dec-2005) (Proof shortened by Raph Levien, 30-Jun-2006)

	Ref	Expression
Assertion	class2seteq	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		ax-1	⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ 𝐴 → 𝐴 ∈ V ) )
3	2	ralrimiv	⊢ ( 𝐴 ∈ V → ∀ 𝑥 ∈ 𝐴 𝐴 ∈ V )
4		rabid2	⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } ↔ ∀ 𝑥 ∈ 𝐴 𝐴 ∈ V )
5	3 4	sylibr	⊢ ( 𝐴 ∈ V → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } )
6	5	eqcomd	⊢ ( 𝐴 ∈ V → { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } = 𝐴 )
7	1 6	syl	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ 𝐴 ∈ V } = 𝐴 )