Theorem sucid 3051

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 2496	. 2 |- A e. {A}
3		df-suc 2981	. . . . . 6 |- suc A = (A u. {A})
4	3	eleq2i 1581	. . . . 5 |- (A e. suc A <-> A e. (A u. {A}))
5		elun 2225	. . . . 5 |- (A e. (A u. {A}) <-> (A e. A \/ A e. {A}))
6	4, 5	bitri 171	. . . 4 |- (A e. suc A <-> (A e. A \/ A e. {A}))
7	6	biimpri 150	. . 3 |- ((A e. A \/ A e. {A}) -> A e. suc A)
8	7	olcs 273	. 2 |- (A e. {A} -> A e. suc A)
9	2, 8	ax-mp 7	1 |- A e. suc A

Syntax hints:   \/ wo 220   e. wcel 994  Vcvv 1857   u. cun 2097  {csn 2467  suc csuc 2977

This theorem is referenced by:  sucidg 3052  eqelsuc 3054  unon 3185  onuninsuci 3194  tfinds 3212  peano5 3241  tz7.44-2 4230  oawordeulem 4324  oalimcl 4330  omlimcl 4345  oneo 4348  oeworde 4356  ac6sfilem2 4589  ac6sfilem3 4590  ac6sfi 4591  phplem4 4658  php 4660  unifi 4701  fiint 4703  fodomfi 4709  inf0 4751  oancom 4779  r1val1 4804  rankwflem 4811  rankr1 4820  rankxplim3 4860  cardlim 5001  cardaleph 5035  finsschain 11425  infenomsub 11450  fbssint 11626  fcluscomplem 11732

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-sn 2470  df-pr 2471  df-suc 2981

Copyright terms: Public domain