Metamath Proof Explorer
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 ) |