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 ⊢≀∅=yz|∃xy∈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 ⊢∃xy∈x∅∧z∈x∅↔∃xy∈∅∧z∈∅
7 19.9v ⊢∃xy∈∅∧z∈∅↔y∈∅∧z∈∅
8 6 7 bitri ⊢∃xy∈x∅∧z∈x∅↔y∈∅∧z∈∅
9 8 opabbii ⊢yz|∃xy∈x∅∧z∈x∅=yz|y∈∅∧z∈∅
10 prnzg ⊢y∈V→yz≠∅
11 10 elv ⊢yz≠∅
12 ss0b ⊢yz⊆∅↔yz=∅
13 11 12 nemtbir ⊢¬yz⊆∅
14 prssg ⊢y∈V∧z∈V→y∈∅∧z∈∅↔yz⊆∅
15 14 el2v ⊢y∈∅∧z∈∅↔yz⊆∅
16 13 15 mtbir ⊢¬y∈∅∧z∈∅
17 16 opabf ⊢yz|y∈∅∧z∈∅=∅
18 1 9 17 3eqtri ⊢≀∅=∅