Metamath Proof Explorer


Theorem cosscnvex

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

Ref Expression
Assertion cosscnvex ⊢ A ∈ V → ≀ A -1 ∈ V

Proof

Step Hyp Ref Expression
1 cnvexg ⊢ A ∈ V → A -1 ∈ V
2 cossex ⊢ A -1 ∈ V → ≀ A -1 ∈ V
3 1 2 syl ⊢ A ∈ V → ≀ A -1 ∈ V