Theorem bj-elsn0 37199

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 4587 and elsn2g 4614 (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 4590	. 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
2		bj-inexeqex 37198	. . . . 5 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3		simpl 482	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
4		elsng 4587	. . . . . 6 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
5	4	biimprd 248	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 = 𝐵 → 𝐴 ∈ {𝐵}))
6	2, 3, 5	3syl 18	. . . 4 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝐴 = 𝐵 → 𝐴 ∈ {𝐵}))
7	6	ex 412	. . 3 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 = 𝐵 → (𝐴 = 𝐵 → 𝐴 ∈ {𝐵})))
8	7	pm2.43d 53	. 2 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ∈ {𝐵}))
9	1, 8	impbid2 226	1 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∩ cin 3896  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-sn 4574

This theorem is referenced by: (None)