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

Metamath Proof Explorer

Theorem dmsnopg

Description: The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion dmsnopg ⊢ B ∈ V → dom ⁡ A B = A

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 vex ⊢ y ∈ V
3 1 2 opth1 ⊢ x y = A B → x = A
4 3 exlimiv ⊢ ∃ y x y = A B → x = A
5 opeq1 ⊢ x = A → x B = A B
6 opeq2 ⊢ y = B → x y = x B
7 6 eqeq1d ⊢ y = B → x y = A B ↔ x B = A B
8 7 spcegv ⊢ B ∈ V → x B = A B → ∃ y x y = A B
9 5 8 syl5 ⊢ B ∈ V → x = A → ∃ y x y = A B
10 4 9 impbid2 ⊢ B ∈ V → ∃ y x y = A B ↔ x = A
11 1 eldm2 ⊢ x ∈ dom ⁡ A B ↔ ∃ y x y ∈ A B
12 opex ⊢ x y ∈ V
13 12 elsn ⊢ x y ∈ A B ↔ x y = A B
14 13 exbii ⊢ ∃ y x y ∈ A B ↔ ∃ y x y = A B
15 11 14 bitri ⊢ x ∈ dom ⁡ A B ↔ ∃ y x y = A B
16 velsn ⊢ x ∈ A ↔ x = A
17 10 15 16 3bitr4g ⊢ B ∈ V → x ∈ dom ⁡ A B ↔ x ∈ A
18 17 eqrdv ⊢ B ∈ V → dom ⁡ A B = A