Theorem bj-inexeqex

Description: Lemma for bj-opelid (but not specific to the identity relation): if the intersection of two classes is a set and the two classes are equal, then both are sets (all three classes are equal, so they all belong to V , but it is more convenient to have _V in the consequent for theorems using it). (Contributed by BJ, 27-Dec-2023)

	Ref	Expression
Assertion	bj-inexeqex	$$⊢\left(A\cap B\in V\wedge A=B\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$$⊢A=B\to A\subseteq B$$
2		df-ss	$$⊢A\subseteq B\leftrightarrow A\cap B=A$$
3	1 2	sylib	$$⊢A=B\to A\cap B=A$$
4		eleq1	$$⊢A\cap B=A\to \left(A\cap B\in V\leftrightarrow A\in V\right)$$
5	4	biimpac	$$⊢\left(A\cap B\in V\wedge A\cap B=A\right)\to A\in V$$
6	3 5	sylan2	$$⊢\left(A\cap B\in V\wedge A=B\right)\to A\in V$$
7	6	elexd	$$⊢\left(A\cap B\in V\wedge A=B\right)\to A\in \mathrm{V}$$
8		eqimss2	$$⊢A=B\to B\subseteq A$$
9		sseqin2	$$⊢B\subseteq A\leftrightarrow A\cap B=B$$
10	8 9	sylib	$$⊢A=B\to A\cap B=B$$
11		eleq1	$$⊢A\cap B=B\to \left(A\cap B\in V\leftrightarrow B\in V\right)$$
12	11	biimpac	$$⊢\left(A\cap B\in V\wedge A\cap B=B\right)\to B\in V$$
13	10 12	sylan2	$$⊢\left(A\cap B\in V\wedge A=B\right)\to B\in V$$
14	13	elexd	$$⊢\left(A\cap B\in V\wedge A=B\right)\to B\in \mathrm{V}$$
15	7 14	jca	$$⊢\left(A\cap B\in V\wedge A=B\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$