Metamath Proof Explorer

Theorem cossex

Description: If A is a set then the class of cosets by A is a set. (Contributed by Peter Mazsa, 4-Jan-2019)

Ref Expression
Assertion cossex 
|- ( A e. V -> ,~ A e. _V )

Proof

Step Hyp Ref Expression
1 dfcoss3 
 |-  ,~ A = ( A o. `' A )
2 cnvexg 
 |-  ( A e. V -> `' A e. _V )
3 coexg 
 |-  ( ( A e. V /\ `' A e. _V ) -> ( A o. `' A ) e. _V )
4 2 3 mpdan 
 |-  ( A e. V -> ( A o. `' A ) e. _V )
5 1 4 eqeltrid 
 |-  ( A e. V -> ,~ A e. _V )