Theorem elinsn

Description: If the intersection of two classes is a (proper) singleton, then the singleton element is a member of both classes. (Contributed by AV, 30-Dec-2021)

	Ref	Expression
Assertion	elinsn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∩ 𝐶 ) = { 𝐴 } ) → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
2		eleq2	⊢ ( ( 𝐵 ∩ 𝐶 ) = { 𝐴 } → ( 𝐴 ∈ ( 𝐵 ∩ 𝐶 ) ↔ 𝐴 ∈ { 𝐴 } ) )
3		elin	⊢ ( 𝐴 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )
4	3	biimpi	⊢ ( 𝐴 ∈ ( 𝐵 ∩ 𝐶 ) → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )
5	2 4	biimtrrdi	⊢ ( ( 𝐵 ∩ 𝐶 ) = { 𝐴 } → ( 𝐴 ∈ { 𝐴 } → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) )
6	1 5	mpan9	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∩ 𝐶 ) = { 𝐴 } ) → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )