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	|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
Assertion	prtex	|- ( Prt A -> ( .~ e. _V <-> A e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		prtlem18.1	|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2	1	prter1	|- ( Prt A -> .~ Er U. A )
3		erexb	|- ( .~ Er U. A -> ( .~ e. _V <-> U. A e. _V ) )
4	2 3	syl	|- ( Prt A -> ( .~ e. _V <-> U. A e. _V ) )
5		uniexb	|- ( A e. _V <-> U. A e. _V )
6	4 5	bitr4di	|- ( Prt A -> ( .~ e. _V <-> A e. _V ) )