Theorem bj-elsn0 37827

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 4602 and elsn2g 4629 (which could be proved from it). (Contributed by BJ, 20-Jan-2024.)

Assertion

Ref	Expression
bj-elsn0	⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Proof of Theorem bj-elsn0

Step	Hyp	Ref	Expression
1		elsni 4605	. 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
2		bj-inexeqex 37826	. . . . 5 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3		simpl 487	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
4		elsng 4602	. . . . . 6 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
5	4	biimprd 251	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 = 𝐵 → 𝐴 ∈ {𝐵}))
6	2, 3, 5	3syl 19	. . . 4 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝐴 = 𝐵 → 𝐴 ∈ {𝐵}))
7	6	ex 417	. . 3 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 = 𝐵 → (𝐴 = 𝐵 → 𝐴 ∈ {𝐵})))
8	7	pm2.43d 54	. 2 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ∈ {𝐵}))
9	1, 8	impbid2 229	1 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1569   ∈ wcel 2142  Vcvv 3454   ∩ cin 3903  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921  df-sn 4589

This theorem is used by: (None)