Theorem bj-elsn0

Description: If the intersection of two classes is a set, then these classes are equal if and only if one is an element of the singleton formed on the other. Stronger form of elsng and elsn2g (which could be proved from it). (Contributed by BJ, 20-Jan-2024)

	Ref	Expression
Assertion	bj-elsn0	|- ( ( A i^i B ) e. V -> ( A e. { B } <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		elsni	|- ( A e. { B } -> A = B )
2		bj-inexeqex	|- ( ( ( A i^i B ) e. V /\ A = B ) -> ( A e. _V /\ B e. _V ) )
3		simpl	|- ( ( A e. _V /\ B e. _V ) -> A e. _V )
4		elsng	|- ( A e. _V -> ( A e. { B } <-> A = B ) )
5	4	biimprd	|- ( A e. _V -> ( A = B -> A e. { B } ) )
6	2 3 5	3syl	|- ( ( ( A i^i B ) e. V /\ A = B ) -> ( A = B -> A e. { B } ) )
7	6	ex	|- ( ( A i^i B ) e. V -> ( A = B -> ( A = B -> A e. { B } ) ) )
8	7	pm2.43d	|- ( ( A i^i B ) e. V -> ( A = B -> A e. { B } ) )
9	1 8	impbid2	|- ( ( A i^i B ) e. V -> ( A e. { B } <-> A = B ) )