MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsuc2g Structured version   Visualization version   GIF version

Theorem elsuc2g 6437
Description: Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.)
Assertion
Ref Expression
elsuc2g (𝐵𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))

Proof of Theorem elsuc2g
StepHypRef Expression
1 df-suc 6374 . . 3 suc 𝐵 = (𝐵 ∪ {𝐵})
21eleq2i 2818 . 2 (𝐴 ∈ suc 𝐵𝐴 ∈ (𝐵 ∪ {𝐵}))
3 elun 4145 . . 3 (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
4 elsn2g 4661 . . . 4 (𝐵𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
54orbi2d 913 . . 3 (𝐵𝑉 → ((𝐴𝐵𝐴 ∈ {𝐵}) ↔ (𝐴𝐵𝐴 = 𝐵)))
63, 5bitrid 282 . 2 (𝐵𝑉 → (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 = 𝐵)))
72, 6bitrid 282 1 (𝐵𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wo 845   = wceq 1534  wcel 2099  cun 3944  {csn 4623  suc csuc 6370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3951  df-sn 4624  df-suc 6374
This theorem is referenced by:  elsuc2  6439  om2uzlti  13964
  Copyright terms: Public domain W3C validator