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 )