This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )