Description: If the intersection of two classes is a set, then these classes are equal if and only if one is an element of the singleton formed on the other. Stronger form of elsng and elsn2g (which could be proved from it). (Contributed by BJ, 20-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-elsn0 | ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elsni | ⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 ) | |
| 2 | bj-inexeqex | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) | |
| 3 | simpl | ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐴 ∈ V ) | |
| 4 | elsng | ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) ) | |
| 5 | 4 | biimprd | ⊢ ( 𝐴 ∈ V → ( 𝐴 = 𝐵 → 𝐴 ∈ { 𝐵 } ) ) |
| 6 | 2 3 5 | 3syl | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( 𝐴 = 𝐵 → 𝐴 ∈ { 𝐵 } ) ) |
| 7 | 6 | ex | ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 = 𝐵 → ( 𝐴 = 𝐵 → 𝐴 ∈ { 𝐵 } ) ) ) |
| 8 | 7 | pm2.43d | ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 = 𝐵 → 𝐴 ∈ { 𝐵 } ) ) |
| 9 | 1 8 | impbid2 | ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) ) |