Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bdeqsuc Structured version   GIF version

Theorem bdeqsuc 7255
Description: Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
Assertion
Ref Expression
bdeqsuc BOUNDED x = suc y
Distinct variable group:   x,y

Proof of Theorem bdeqsuc
StepHypRef Expression
1 bdcsuc 7254 . . . 4 BOUNDED suc y
21bdss 7238 . . 3 BOUNDED x ⊆ suc y
3 bdcv 7222 . . . . . . 7 BOUNDED x
43bdss 7238 . . . . . 6 BOUNDED yx
53bdsnss 7247 . . . . . 6 BOUNDED {y} ⊆ x
64, 5ax-bdan 7189 . . . . 5 BOUNDED (yx {y} ⊆ x)
7 unss 3094 . . . . 5 ((yx {y} ⊆ x) ↔ (y ∪ {y}) ⊆ x)
86, 7bd0 7198 . . . 4 BOUNDED (y ∪ {y}) ⊆ x
9 df-suc 4057 . . . . 5 suc y = (y ∪ {y})
109sseq1i 2946 . . . 4 (suc yx ↔ (y ∪ {y}) ⊆ x)
118, 10bd0r 7199 . . 3 BOUNDED suc yx
122, 11ax-bdan 7189 . 2 BOUNDED (x ⊆ suc y suc yx)
13 eqss 2937 . 2 (x = suc y ↔ (x ⊆ suc y suc yx))
1412, 13bd0r 7199 1 BOUNDED x = suc y
Colors of variables: wff set class
Syntax hints:   wa 97   = wceq 1228  cun 2892  wss 2894  {csn 3350  suc csuc 4051  BOUNDED wbd 7186
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-bd0 7187  ax-bdan 7189  ax-bdor 7190  ax-bdal 7192  ax-bdeq 7194  ax-bdel 7195  ax-bdsb 7196
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-v 2537  df-un 2899  df-in 2901  df-ss 2908  df-sn 3356  df-suc 4057  df-bdc 7215
This theorem is referenced by:  bj-bdsucel  7256  bj-nn0suc0  7319
  Copyright terms: Public domain W3C validator