Theorem sucidg 3743

Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (The proof was shortened by Scott Fenton, 20-Feb-2012.)

Assertion

Ref	Expression
sucidg	|- (A e. B -> A e. suc A)

Proof of Theorem sucidg

Step	Hyp	Ref	Expression
1		eqid 1884	. . 3 |- A = A
2	1	olci 293	. 2 |- (A e. A \/ A = A)
3		elsucg 3732	. 2 |- (A e. B -> (A e. suc A <-> (A e. A \/ A = A)))
4	2, 3	mpbiri 211	1 |- (A e. B -> A e. suc A)

Syntax hints:   -> wi 3   \/ wo 239   = wceq 1298   e. wcel 1300  suc csuc 3659

This theorem is referenced by:  sucid 3744  nsuceq0 3749  trsuc 3752  trsucOLD 3753  sucssel 3763  ordsuc 3895  onsucuni2OLD 3915  nlimsucg 3923  nlimsucgOLD 3924  tfrlem13 5131  oarec 5244  oeordi 5262  php4 5610  suc11reg 5710  tarsuc3 15246

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-suc 3663

Copyright terms: Public domain