Users' Mathboxes 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 36675
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 4646 and elsn2g 4671 (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 4649 . 2 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
2 bj-inexeqex 36674 . . . . 5 (((𝐴𝐵) ∈ 𝑉𝐴 = 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3 simpl 481 . . . . 5 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
4 elsng 4646 . . . . . 6 (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
54biimprd 247 . . . . 5 (𝐴 ∈ V → (𝐴 = 𝐵𝐴 ∈ {𝐵}))
62, 3, 53syl 18 . . . 4 (((𝐴𝐵) ∈ 𝑉𝐴 = 𝐵) → (𝐴 = 𝐵𝐴 ∈ {𝐵}))
76ex 411 . . 3 ((𝐴𝐵) ∈ 𝑉 → (𝐴 = 𝐵 → (𝐴 = 𝐵𝐴 ∈ {𝐵})))
87pm2.43d 53 . 2 ((𝐴𝐵) ∈ 𝑉 → (𝐴 = 𝐵𝐴 ∈ {𝐵}))
91, 8impbid2 225 1 ((𝐴𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  Vcvv 3473  cin 3948  {csn 4632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-in 3956  df-ss 3966  df-sn 4633
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator