Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1256 Structured version   Unicode version

Theorem bnj1256 32361
 Description: Technical lemma for bnj60 32408. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1256.1
bnj1256.2
bnj1256.3
bnj1256.4
bnj1256.5
bnj1256.6
bnj1256.7
Assertion
Ref Expression
bnj1256
Distinct variable groups:   ,   ,,   ,,   ,   ,   ,,   ,,
Allowed substitution hints:   (,,,,,)   (,,,,,)   (,,,,)   (,,,)   (,,,,,)   (,,,,,)   (,,,,)   (,,,,,)   (,,,)   (,,,,)

Proof of Theorem bnj1256
StepHypRef Expression
1 bnj1256.6 . 2
2 abid 2441 . . . 4
32bnj1238 32155 . . 3
4 bnj1256.2 . . . 4
5 bnj1256.3 . . . 4
6 eqid 2454 . . . 4
7 eqid 2454 . . . 4
84, 5, 6, 7bnj1234 32359 . . 3
93, 8eleq2s 2562 . 2
101, 9bnj770 32111 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   w3a 965   wceq 1370   wcel 1758  cab 2439   wne 2648  wral 2799  wrex 2800  crab 2803   cin 3438   wss 3439  cop 3994   class class class wbr 4403   cdm 4951   cres 4953   wfn 5524  cfv 5529   w-bnj17 32029   c-bnj14 32031   w-bnj15 32035 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 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-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-res 4963  df-iota 5492  df-fun 5531  df-fn 5532  df-fv 5537  df-bnj17 32030 This theorem is referenced by:  bnj1253  32363  bnj1286  32365  bnj1280  32366
 Copyright terms: Public domain W3C validator