Theorem sucid 3041

Description: A set belongs to its successor.

Hypothesis

Ref	Expression
sucid.1	|- A e. V

Assertion

Ref	Expression
sucid	|- A e. suc A

Proof of Theorem sucid

Step	Hyp	Ref	Expression
1		sucid.1	. . 3 |- A e. V
2	1	snid 2425	. 2 |- A e. {A}
3		df-suc 2944	. . . . . 6 |- suc A = (A u. {A})
4	3	eleq2i 1530	. . . . 5 |- (A e. suc A <-> A e. (A u. {A}))
5		elun 2163	. . . . 5 |- (A e. (A u. {A}) <-> (A e. A \/ A e. {A}))
6	4, 5	bitr 173	. . . 4 |- (A e. suc A <-> (A e. A \/ A e. {A}))
7	6	biimpr 152	. . 3 |- ((A e. A \/ A e. {A}) -> A e. suc A)
8	7	olcs 275	. 2 |- (A e. {A} -> A e. suc A)
9	2, 8	ax-mp 7	1 |- A e. suc A

Syntax hints:   \/ wo 222   e. wcel 955  Vcvv 1802   u. cun 2035  {csn 2399  suc csuc 2940

This theorem is referenced by:  sucidg 3042  eqelsuc 3044  unon 3078  onuninsuc 3098  peano5 3143  tfinds 3151  tz7.44-2 3914  oawordeulem 4172  oalimcl 4178  omlimcl 4193  oneo 4196  oeworde 4204  phplem4 4491  php 4493  unifi 4532  fiint 4534  fodomfi 4540  inf0 4578  oancom 4605  r1val1 4630  rankwflem 4637  rankr1 4646  rankxplim3 4686  cardlim 4823  cardaleph 4857

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-suc 2944

Copyright terms: Public domain