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

Proof

Step	Hyp	Ref	Expression
1		eqimss	|- ( A = B -> A C_ B )
2		df-ss	|- ( A C_ B <-> ( A i^i B ) = A )
3	1 2	sylib	|- ( A = B -> ( A i^i B ) = A )
4		eleq1	|- ( ( A i^i B ) = A -> ( ( A i^i B ) e. V <-> A e. V ) )
5	4	biimpac	|- ( ( ( A i^i B ) e. V /\ ( A i^i B ) = A ) -> A e. V )
6	3 5	sylan2	|- ( ( ( A i^i B ) e. V /\ A = B ) -> A e. V )
7	6	elexd	|- ( ( ( A i^i B ) e. V /\ A = B ) -> A e. _V )
8		eqimss2	|- ( A = B -> B C_ A )
9		sseqin2	|- ( B C_ A <-> ( A i^i B ) = B )
10	8 9	sylib	|- ( A = B -> ( A i^i B ) = B )
11		eleq1	|- ( ( A i^i B ) = B -> ( ( A i^i B ) e. V <-> B e. V ) )
12	11	biimpac	|- ( ( ( A i^i B ) e. V /\ ( A i^i B ) = B ) -> B e. V )
13	10 12	sylan2	|- ( ( ( A i^i B ) e. V /\ A = B ) -> B e. V )
14	13	elexd	|- ( ( ( A i^i B ) e. V /\ A = B ) -> B e. _V )
15	7 14	jca	|- ( ( ( A i^i B ) e. V /\ A = B ) -> ( A e. _V /\ B e. _V ) )