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	|- ( ( A e. V /\ ( B i^i C ) = { A } ) -> ( A e. B /\ A e. C ) )

Proof

Step	Hyp	Ref	Expression
1		snidg	|- ( A e. V -> A e. { A } )
2		eleq2	|- ( ( B i^i C ) = { A } -> ( A e. ( B i^i C ) <-> A e. { A } ) )
3		elin	|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
4	3	biimpi	|- ( A e. ( B i^i C ) -> ( A e. B /\ A e. C ) )
5	2 4	biimtrrdi	|- ( ( B i^i C ) = { A } -> ( A e. { A } -> ( A e. B /\ A e. C ) ) )
6	1 5	mpan9	|- ( ( A e. V /\ ( B i^i C ) = { A } ) -> ( A e. B /\ A e. C ) )