Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-elsn0 Structured version   Visualization version   GIF version

Theorem bj-elsn0 34885
 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 4539 and elsn2g 4563 (which could be proved from it). (Contributed by BJ, 20-Jan-2024.)
Assertion
Ref Expression
bj-elsn0 ((𝐴𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Proof of Theorem bj-elsn0
StepHypRef Expression
1 elsni 4542 . 2 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
2 bj-inexeqex 34884 . . . . 5 (((𝐴𝐵) ∈ 𝑉𝐴 = 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3 simpl 486 . . . . 5 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
4 elsng 4539 . . . . . 6 (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
54biimprd 251 . . . . 5 (𝐴 ∈ V → (𝐴 = 𝐵𝐴 ∈ {𝐵}))
62, 3, 53syl 18 . . . 4 (((𝐴𝐵) ∈ 𝑉𝐴 = 𝐵) → (𝐴 = 𝐵𝐴 ∈ {𝐵}))
76ex 416 . . 3 ((𝐴𝐵) ∈ 𝑉 → (𝐴 = 𝐵 → (𝐴 = 𝐵𝐴 ∈ {𝐵})))
87pm2.43d 53 . 2 ((𝐴𝐵) ∈ 𝑉 → (𝐴 = 𝐵𝐴 ∈ {𝐵}))
91, 8impbid2 229 1 ((𝐴𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3409   ∩ cin 3859  {csn 4525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-in 3867  df-ss 3877  df-sn 4526 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator