Theorem sucid 5947

Description: A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)

Hypothesis

Ref	Expression
sucid.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
sucid	⊢ 𝐴 ∈ suc 𝐴

Proof of Theorem sucid

Step	Hyp	Ref	Expression
1		sucid.1	. 2 ⊢ 𝐴 ∈ V
2		sucidg 5946	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ suc 𝐴

Syntax hints:   ∈ wcel 2144  Vcvv 3349  suc csuc 5868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726  df-sn 4315  df-suc 5872

This theorem is referenced by:  eqelsuc  5949  unon  7177  onuninsuci  7186  tfinds  7205  peano5  7235  tfrlem16  7641  oawordeulem  7787  oalimcl  7793  omlimcl  7811  oneo  7814  omeulem1  7815  oeworde  7826  nnawordex  7870  nnneo  7884  phplem4  8297  php  8299  fiint  8392  inf0  8681  oancom  8711  cantnfval2  8729  cantnflt  8732  cantnflem1  8749  cnfcom  8760  cnfcom2  8762  cnfcom3lem  8763  cnfcom3  8764  r1val1  8812  rankxplim3  8907  cardlim  8997  fseqenlem1  9046  cardaleph  9111  pwsdompw  9227  cfsmolem  9293  axdc3lem4  9476  ttukeylem5  9536  ttukeylem6  9537  ttukeylem7  9538  canthp1lem2  9676  pwxpndom2  9688  winainflem  9716  winalim2  9719  nqereu  9952  bnj216  31132  bnj98  31269  dfrdg2  32031  dford3lem2  38113  pw2f1ocnv  38123  aomclem1  38143