Metamath Proof Explorer


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 df-ss ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = 𝐴 )
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 ) )