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 ( 𝐴𝑉 → ≀ 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 dfcoss3 𝐴 = ( 𝐴 𝐴 )
2 cnvexg ( 𝐴𝑉 𝐴 ∈ V )
3 coexg ( ( 𝐴𝑉 𝐴 ∈ V ) → ( 𝐴 𝐴 ) ∈ V )
4 2 3 mpdan ( 𝐴𝑉 → ( 𝐴 𝐴 ) ∈ V )
5 1 4 eqeltrid ( 𝐴𝑉 → ≀ 𝐴 ∈ V )