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 6383 is sucidVD 42821 without virtual deductions and was automatically
derived from sucidVD 42821.
|
Ref | Expression |
---|---|
sucidVD.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
sucidVD | ⊢ 𝐴 ∈ suc 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sucidVD.1 | . . . 4 ⊢ 𝐴 ∈ V | |
2 | 1 | snid 4609 | . . 3 ⊢ 𝐴 ∈ {𝐴} |
3 | elun2 4124 | . . 3 ⊢ (𝐴 ∈ {𝐴} → 𝐴 ∈ (𝐴 ∪ {𝐴})) | |
4 | 2, 3 | e0a 42721 | . 2 ⊢ 𝐴 ∈ (𝐴 ∪ {𝐴}) |
5 | df-suc 6308 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
6 | 4, 5 | eleqtrri 2836 | 1 ⊢ 𝐴 ∈ suc 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3441 ∪ cun 3896 {csn 4573 suc csuc 6304 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3443 df-un 3903 df-in 3905 df-ss 3915 df-sn 4574 df-suc 6308 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |