Metamath Proof Explorer

Theorem coss0

Description: Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019)

Ref Expression
Assertion coss0 ⊢ ≀ ∅ = ∅

Proof

Step Hyp Ref Expression
1 dfcoss2 ⊢ ≀ ∅ = y z | ∃ x y ∈ x ∅ ∧ z ∈ x ∅
2 ec0 ⊢ x ∅ = ∅
3 2 eleq2i ⊢ y ∈ x ∅ ↔ y ∈ ∅
4 2 eleq2i ⊢ z ∈ x ∅ ↔ z ∈ ∅
5 3 4 anbi12i ⊢ y ∈ x ∅ ∧ z ∈ x ∅ ↔ y ∈ ∅ ∧ z ∈ ∅
6 5 exbii ⊢ ∃ x y ∈ x ∅ ∧ z ∈ x ∅ ↔ ∃ x y ∈ ∅ ∧ z ∈ ∅
7 19.9v ⊢ ∃ x y ∈ ∅ ∧ z ∈ ∅ ↔ y ∈ ∅ ∧ z ∈ ∅
8 6 7 bitri ⊢ ∃ x y ∈ x ∅ ∧ z ∈ x ∅ ↔ y ∈ ∅ ∧ z ∈ ∅
9 8 opabbii ⊢ y z | ∃ x y ∈ x ∅ ∧ z ∈ x ∅ = y z | y ∈ ∅ ∧ z ∈ ∅
10 prnzg ⊢ y ∈ V → y z ≠ ∅
11 10 elv ⊢ y z ≠ ∅
12 ss0b ⊢ y z ⊆ ∅ ↔ y z = ∅
13 11 12 nemtbir ⊢ ¬ y z ⊆ ∅
14 prssg ⊢ y ∈ V ∧ z ∈ V → y ∈ ∅ ∧ z ∈ ∅ ↔ y z ⊆ ∅
15 14 el2v ⊢ y ∈ ∅ ∧ z ∈ ∅ ↔ y z ⊆ ∅
16 13 15 mtbir ⊢ ¬ y ∈ ∅ ∧ z ∈ ∅
17 16 opabf ⊢ y z | y ∈ ∅ ∧ z ∈ ∅ = ∅
18 1 9 17 3eqtri ⊢ ≀ ∅ = ∅