Theorem prid1

Description: An unordered pair contains its first member. Part of Theorem 7.6 of Quine p. 49. (Contributed by NM, 24-Jun-1993)

	Ref	Expression
Hypothesis	prid1.1	⊢ 𝐴 ∈ V
Assertion	prid1	⊢ 𝐴 ∈ { 𝐴 , 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		prid1.1	⊢ 𝐴 ∈ V
2		prid1g	⊢ ( 𝐴 ∈ V → 𝐴 ∈ { 𝐴 , 𝐵 } )
3	1 2	ax-mp	⊢ 𝐴 ∈ { 𝐴 , 𝐵 }