Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  onfrALTlem5 Unicode version

Theorem onfrALTlem5 32093
Description: Lemma for onfrALT 32100. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTlem5
Distinct variable groups:   , ,   , ,

Proof of Theorem onfrALTlem5
StepHypRef Expression
1 vex 3084 . . . 4
21inex1 4550 . . 3
3 sbcimg 3339 . . 3
42, 3ax-mp 5 . 2
5 sbcan 3340 . . . 4
6 sseq1 3491 . . . . . 6
72, 6sbcie 3332 . . . . 5
8 df-ne 2650 . . . . . . 7
98sbcbii 3357 . . . . . 6
10 sbcng 3338 . . . . . . . 8
1110bicomd 201 . . . . . . 7
122, 11ax-mp 5 . . . . . 6
13 eqsbc3 3337 . . . . . . . 8
142, 13ax-mp 5 . . . . . . 7
1514necon3bbii 2714 . . . . . 6
169, 12, 153bitr2i 273 . . . . 5
177, 16anbi12i 697 . . . 4
185, 17bitri 249 . . 3
19 df-rex 2806 . . . . 5
2019sbcbii 3357 . . . 4
21 sbcan 3340 . . . . . . 7
22 sbcel2gv 3364 . . . . . . . . 9
232, 22ax-mp 5 . . . . . . . 8
24 sbceqg 3791 . . . . . . . . . 10
252, 24ax-mp 5 . . . . . . . . 9
26 csbin 3826 . . . . . . . . . . 11
27 csbvarg 3814 . . . . . . . . . . . . 13
282, 27ax-mp 5 . . . . . . . . . . . 12
29 csbconstg 3414 . . . . . . . . . . . . 13
302, 29ax-mp 5 . . . . . . . . . . . 12
3128, 30ineq12i 3664 . . . . . . . . . . 11
3226, 31eqtri 2483 . . . . . . . . . 10
33 csb0 3788 . . . . . . . . . 10
3432, 33eqeq12i 2474 . . . . . . . . 9
3525, 34bitri 249 . . . . . . . 8
3623, 35anbi12i 697 . . . . . . 7
3721, 36bitri 249 . . . . . 6
3837exbii 1635 . . . . 5
39 sbcex2 3351 . . . . 5
40 df-rex 2806 . . . . 5
4138, 39, 403bitr4i 277 . . . 4
4220, 41bitri 249 . . 3
4318, 42imbi12i 326 . 2
444, 43bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  =wceq 1370  E.wex 1587  e.wcel 1758  =/=wne 2648  E.wrex 2801   cvv 3081  [.wsbc 3297  [_csb 3401  i^icin 3441  C_wss 3442   c0 3751
This theorem is referenced by:  onfrALTlem3  32095  onfrALTlem3VD  32466
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 1955  ax-ext 2432  ax-sep 4530
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rex 2806  df-rab 2809  df-v 3083  df-sbc 3298  df-csb 3402  df-dif 3445  df-in 3449  df-ss 3456  df-nul 3752
  Copyright terms: Public domain W3C validator