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	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		eqimss	⊢ ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )
2		dfss2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
3	1 2	sylib	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
4		eleq1	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
5	4	biimpac	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) → 𝐴 ∈ 𝑉 )
6	3 5	sylan2	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑉 )
7	6	elexd	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ V )
8		eqimss2	⊢ ( 𝐴 = 𝐵 → 𝐵 ⊆ 𝐴 )
9		sseqin2	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
10	8 9	sylib	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐵 )
11		eleq1	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ↔ 𝐵 ∈ 𝑉 ) )
12	11	biimpac	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) → 𝐵 ∈ 𝑉 )
13	10 12	sylan2	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝑉 )
14	13	elexd	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ V )
15	7 14	jca	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )