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 { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )