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

Theorem kmlem5 7825
 Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
Assertion
Ref Expression
kmlem5
Distinct variable group:   ,,

Proof of Theorem kmlem5
StepHypRef Expression
1 difss 3337 . . . 4
2 sslin 3429 . . . 4
31, 2ax-mp 8 . . 3
4 kmlem4 7824 . . 3
53, 4syl5sseq 3260 . 2
6 ss0b 3518 . 2
75, 6sylib 188 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wceq 1633   wcel 1701   wne 2479   cdif 3183   cin 3185   wss 3186  c0 3489  csn 3674  cuni 3864 This theorem is referenced by:  kmlem9  7829 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-v 2824  df-dif 3189  df-in 3193  df-ss 3200  df-nul 3490  df-sn 3680  df-uni 3865
 Copyright terms: Public domain W3C validator