![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sucidVD | Structured version Visualization version GIF version |
Description: A set belongs to its successor. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools
program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant.
sucid 6468 is sucidVD 44870 without virtual deductions and was automatically
derived from sucidVD 44870.
|
Ref | Expression |
---|---|
sucidVD.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
sucidVD | ⊢ 𝐴 ∈ suc 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sucidVD.1 | . . . 4 ⊢ 𝐴 ∈ V | |
2 | 1 | snid 4667 | . . 3 ⊢ 𝐴 ∈ {𝐴} |
3 | elun2 4193 | . . 3 ⊢ (𝐴 ∈ {𝐴} → 𝐴 ∈ (𝐴 ∪ {𝐴})) | |
4 | 2, 3 | e0a 44770 | . 2 ⊢ 𝐴 ∈ (𝐴 ∪ {𝐴}) |
5 | df-suc 6392 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
6 | 4, 5 | eleqtrri 2838 | 1 ⊢ 𝐴 ∈ suc 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3478 ∪ cun 3961 {csn 4631 suc csuc 6388 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-un 3968 df-ss 3980 df-sn 4632 df-suc 6392 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |