|   | 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 6466 is sucidVD 44892 without virtual deductions and was automatically
       derived from sucidVD 44892. 
 | 
| Ref | Expression | 
|---|---|
| sucidVD.1 | ⊢ 𝐴 ∈ V | 
| Ref | Expression | 
|---|---|
| sucidVD | ⊢ 𝐴 ∈ suc 𝐴 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | sucidVD.1 | . . . 4 ⊢ 𝐴 ∈ V | |
| 2 | 1 | snid 4662 | . . 3 ⊢ 𝐴 ∈ {𝐴} | 
| 3 | elun2 4183 | . . 3 ⊢ (𝐴 ∈ {𝐴} → 𝐴 ∈ (𝐴 ∪ {𝐴})) | |
| 4 | 2, 3 | e0a 44792 | . 2 ⊢ 𝐴 ∈ (𝐴 ∪ {𝐴}) | 
| 5 | df-suc 6390 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
| 6 | 4, 5 | eleqtrri 2840 | 1 ⊢ 𝐴 ∈ suc 𝐴 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∪ cun 3949 {csn 4626 suc csuc 6386 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-ss 3968 df-sn 4627 df-suc 6390 | 
| This theorem is referenced by: (None) | 
| Copyright terms: Public domain | W3C validator |