Theorem bj-elsn0 37121

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 4662 and elsn2g 4686 (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 4665	. 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
2		bj-inexeqex 37120	. . . . 5 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3		simpl 482	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
4		elsng 4662	. . . . . 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 1537   ∈ wcel 2108  Vcvv 3488   ∩ cin 3975  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-sn 4649

This theorem is referenced by: (None)