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 ( 𝐵 ∈ 𝑉 → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 vex ⊢ 𝑦 ∈ V
3 1 2 opth1 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → 𝑥 = 𝐴 )
4 3 exlimiv ⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → 𝑥 = 𝐴 )
5 opeq1 ⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
6 opeq2 ⊢ ( 𝑦 = 𝐵 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝐵 ⟩ )
7 6 eqeq1d ⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝑥 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
8 7 spcegv ⊢ ( 𝐵 ∈ 𝑉 → ( ⟨ 𝑥 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
9 5 8 syl5 ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 = 𝐴 → ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
10 4 9 impbid2 ⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 = 𝐴 ) )
11 1 eldm2 ⊢ ( 𝑥 ∈ dom { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } )
12 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
13 12 elsn ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
14 13 exbii ⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
15 11 14 bitri ⊢ ( 𝑥 ∈ dom { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
16 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
17 10 15 16 3bitr4g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ∈ dom { ⟨ 𝐴 , 𝐵 ⟩ } ↔ 𝑥 ∈ { 𝐴 } ) )
18 17 eqrdv ⊢ ( 𝐵 ∈ 𝑉 → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )