Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  istos Structured version   Unicode version

Theorem istos 15307
 Description: The predicate "is a toset." (Contributed by FL, 17-Nov-2014.)
Hypotheses
Ref Expression
istos.b
istos.l
Assertion
Ref Expression
istos Toset
Distinct variable groups:   ,,   , ,
Allowed substitution hints:   (,)

Proof of Theorem istos
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5789 . . . . . 6
2 dfsbcq 3286 . . . . . 6
31, 2syl 16 . . . . 5
43sbcbidv 3343 . . . 4
5 fveq2 5789 . . . . 5
6 dfsbcq 3286 . . . . 5
75, 6syl 16 . . . 4
84, 7bitrd 253 . . 3
9 fvex 5799 . . . 4
10 fvex 5799 . . . 4
11 istos.b . . . . . 6
12 eqtr 2477 . . . . . . . . 9
13 istos.l . . . . . . . . . 10
14 eqtr 2477 . . . . . . . . . . . . 13
15 breq 4392 . . . . . . . . . . . . . . . . 17
16 breq 4392 . . . . . . . . . . . . . . . . 17
1715, 16orbi12d 709 . . . . . . . . . . . . . . . 16
18172ralbidv 2861 . . . . . . . . . . . . . . 15
19 raleq 3013 . . . . . . . . . . . . . . . 16
2019raleqbi1dv 3021 . . . . . . . . . . . . . . 15
2118, 20sylan9bb 699 . . . . . . . . . . . . . 14
2221ex 434 . . . . . . . . . . . . 13
2314, 22syl 16 . . . . . . . . . . . 12
2423expcom 435 . . . . . . . . . . 11
2524eqcoms 2463 . . . . . . . . . 10
2613, 25ax-mp 5 . . . . . . . . 9
2712, 26syl5com 30 . . . . . . . 8
2827expcom 435 . . . . . . 7
2928eqcoms 2463 . . . . . 6
3011, 29ax-mp 5 . . . . 5
3130imp 429 . . . 4
329, 10, 31sbc2ie 3360 . . 3
338, 32syl6bb 261 . 2
34 df-toset 15306 . 2 Toset
3533, 34elrab2 3216 1 Toset
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wo 368   wa 369   wceq 1370   wcel 1758  wral 2795  wsbc 3284   class class class wbr 4390  cfv 5516  cbs 14276  cple 14347  cpo 15212  Tosetctos 15305 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-nul 4519 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-toset 15306 This theorem is referenced by:  tosso  15308  zntoslem  18098  tospos  26253  resstos  26255  tleile  26256  odutos  26258  xrstos  26274  xrge0omnd  26308
 Copyright terms: Public domain W3C validator