Metamath Proof Explorer


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 | u A x u y u
Assertion prtex Prt A ˙ V A V

Proof

Step Hyp Ref Expression
1 prtlem18.1 ˙ = x y | u A x u y u
2 1 prter1 Prt A ˙ Er A
3 erexb ˙ Er A ˙ V A V
4 2 3 syl Prt A ˙ V A V
5 uniexb A V A V
6 4 5 bitr4di Prt A ˙ V A V