Theorem bj-elsn12g

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

	Ref	Expression
Assertion	bj-elsn12g	$$⊢\left(A\in V\vee B\in W\right)\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elsng	$$⊢A\in V\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$
2		elsn2g	$$⊢B\in W\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$
3	1 2	jaoi	$$⊢\left(A\in V\vee B\in W\right)\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$