Theorem bj-elsn12g

Description: Join of elsng and elsn2g . (Contributed by BJ, 18-Nov-2023)

	Ref	Expression
Assertion	bj-elsn12g	|- ( ( A e. V \/ B e. W ) -> ( A e. { B } <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		elsng	|- ( A e. V -> ( A e. { B } <-> A = B ) )
2		elsn2g	|- ( B e. W -> ( A e. { B } <-> A = B ) )
3	1 2	jaoi	|- ( ( A e. V \/ B e. W ) -> ( A e. { B } <-> A = B ) )