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 2736 | . . 3 ⊢ 𝐴 = 𝐴 | |
2 | 1 | olci 864 | . 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴) |
3 | elsucg 6383 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴))) | |
4 | 2, 3 | mpbiri 257 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 845 = wceq 1541 ∈ wcel 2106 suc csuc 6317 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3445 df-un 3913 df-sn 4585 df-suc 6321 |
This theorem is referenced by: sucid 6397 nsuceq0 6398 trsuc 6402 sucssel 6410 ordsuc 7744 ordsucOLD 7745 onpsssuc 7750 nlimsucg 7774 tfrlem11 8330 tfrlem13 8332 tz7.44-2 8349 omeulem1 8525 oeordi 8530 oeeulem 8544 dif1enlem 9096 dif1enlemOLD 9097 rexdif1en 9098 rexdif1enOLD 9099 dif1en 9100 dif1enOLD 9102 php4 9153 wofib 9477 suc11reg 9551 cantnfle 9603 cantnflt2 9605 cantnfp1lem3 9612 cantnflem1 9621 dfac12lem1 10075 dfac12lem2 10076 ttukeylem3 10443 ttukeylem7 10447 r1wunlim 10669 noresle 27029 nosupprefixmo 27032 noinfprefixmo 27033 fmla 33844 ex-sategoelelomsuc 33889 ontgval 34870 sucneqond 35803 finxpreclem4 35832 finxpsuclem 35835 onexgt 41512 onepsuc 41524 ordnexbtwnsuc 41540 nlimsuc 41655 sucomisnotcard 41758 |
Copyright terms: Public domain | W3C validator |