![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sucidg | Structured version Visualization version GIF version |
Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). Lemma 1.7 of [Schloeder] p. 1. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
Ref | Expression |
---|---|
sucidg | ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2728 | . . 3 ⊢ 𝐴 = 𝐴 | |
2 | 1 | olci 865 | . 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴) |
3 | elsucg 6437 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴))) | |
4 | 2, 3 | mpbiri 258 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 = wceq 1534 ∈ wcel 2099 suc csuc 6371 |
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 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-un 3952 df-sn 4630 df-suc 6375 |
This theorem is referenced by: sucid 6451 nsuceq0 6452 trsuc 6456 sucssel 6464 ordsuc 7816 ordsucOLD 7817 onpsssuc 7822 nlimsucg 7846 tfrlem11 8408 tfrlem13 8410 tz7.44-2 8427 omeulem1 8602 oeordi 8607 oeeulem 8621 dif1enlem 9180 dif1enlemOLD 9181 rexdif1en 9182 rexdif1enOLD 9183 dif1en 9184 dif1enOLD 9186 php4 9237 wofib 9568 suc11reg 9642 cantnfle 9694 cantnflt2 9696 cantnfp1lem3 9703 cantnflem1 9712 dfac12lem1 10166 dfac12lem2 10167 ttukeylem3 10534 ttukeylem7 10538 r1wunlim 10760 noresle 27629 nosupprefixmo 27632 noinfprefixmo 27633 fmla 34991 ex-sategoelelomsuc 35036 ontgval 35915 sucneqond 36844 finxpreclem4 36873 finxpsuclem 36876 onexgt 42668 onepsuc 42680 ordnexbtwnsuc 42696 nlimsuc 42871 sucomisnotcard 42974 |
Copyright terms: Public domain | W3C validator |