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

Theorem elsucg 6140
Description: Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.)
Assertion
Ref Expression
elsucg (𝐴𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))

Proof of Theorem elsucg
StepHypRef Expression
1 df-suc 6079 . . . 4 suc 𝐵 = (𝐵 ∪ {𝐵})
21eleq2i 2876 . . 3 (𝐴 ∈ suc 𝐵𝐴 ∈ (𝐵 ∪ {𝐵}))
3 elun 4052 . . 3 (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
42, 3bitri 276 . 2 (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
5 elsng 4492 . . 3 (𝐴𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
65orbi2d 910 . 2 (𝐴𝑉 → ((𝐴𝐵𝐴 ∈ {𝐵}) ↔ (𝐴𝐵𝐴 = 𝐵)))
74, 6syl5bb 284 1 (𝐴𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wo 842   = wceq 1525  wcel 2083  cun 3863  {csn 4478  suc csuc 6075
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-un 3870  df-sn 4479  df-suc 6079
This theorem is referenced by:  elsuc  6142  elelsuc  6145  sucidg  6151  ordsssuc  6159  ordsucelsuc  7400  suc11reg  8935  nlt1pi  10181
  Copyright terms: Public domain W3C validator