Theorem prtex

Description: The equivalence relation generated by a partition is a set if and only if the partition itself is a set. (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypothesis	prtlem18.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
Assertion	prtex	⊢ ( Prt 𝐴 → ( ∼ ∈ V ↔ 𝐴 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		prtlem18.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
2	1	prter1	⊢ ( Prt 𝐴 → ∼ Er ∪ 𝐴 )
3		erexb	⊢ ( ∼ Er ∪ 𝐴 → ( ∼ ∈ V ↔ ∪ 𝐴 ∈ V ) )
4	2 3	syl	⊢ ( Prt 𝐴 → ( ∼ ∈ V ↔ ∪ 𝐴 ∈ V ) )
5		uniexb	⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )
6	4 5	bitr4di	⊢ ( Prt 𝐴 → ( ∼ ∈ V ↔ 𝐴 ∈ V ) )