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

Theorem bnj1039 29776
 Description: Technical lemma for bnj69 29815. 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
bnj1039.1
bnj1039.2
Assertion
Ref Expression
bnj1039

Proof of Theorem bnj1039
StepHypRef Expression
1 bnj1039.2 . 2
2 vex 3084 . . 3
3 bnj1039.1 . . . . 5
4 nfra1 2806 . . . . 5
53, 4nfxfr 1692 . . . 4
65sbcgf 3363 . . 3
72, 6ax-mp 5 . 2
81, 7, 33bitri 274 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wceq 1437   wcel 1868  wral 2775  cvv 3081  wsbc 3299  ciun 4296   csuc 5441  cfv 5598  com 6703   c-bnj14 29489 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-12 1905  ax-13 2053  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-ral 2780  df-v 3083  df-sbc 3300 This theorem is referenced by:  bnj1128  29795
 Copyright terms: Public domain W3C validator