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

Theorem bnj1444 29854
 Description: Technical lemma for bnj60 29873. 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
bnj1444.1
bnj1444.2
bnj1444.3
bnj1444.4
bnj1444.5
bnj1444.6
bnj1444.7
bnj1444.8
bnj1444.9
bnj1444.10
bnj1444.11
bnj1444.12
bnj1444.13
bnj1444.14
bnj1444.15
bnj1444.16
bnj1444.17
bnj1444.18
bnj1444.19
bnj1444.20
Assertion
Ref Expression
bnj1444
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,)   (,,,)   (,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)

Proof of Theorem bnj1444
StepHypRef Expression
1 bnj1444.20 . . 3
2 bnj1444.19 . . . . 5
3 bnj1444.17 . . . . . . 7
4 bnj1444.7 . . . . . . . . 9
5 nfv 1752 . . . . . . . . . 10
6 nfv 1752 . . . . . . . . . 10
7 nfra1 2807 . . . . . . . . . 10
85, 6, 7nf3an 1987 . . . . . . . . 9
94, 8nfxfr 1693 . . . . . . . 8
10 nfv 1752 . . . . . . . 8
119, 10nfan 1985 . . . . . . 7
123, 11nfxfr 1693 . . . . . 6
13 nfv 1752 . . . . . 6
1412, 13nfan 1985 . . . . 5
152, 14nfxfr 1693 . . . 4
16 bnj1444.9 . . . . . 6
17 nfre1 2887 . . . . . . 7
1817nfab 2589 . . . . . 6
1916, 18nfcxfr 2583 . . . . 5
2019nfcri 2578 . . . 4
21 nfv 1752 . . . 4
2215, 20, 21nf3an 1987 . . 3
231, 22nfxfr 1693 . 2
2423nfri 1926 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wa 371   w3a 983  wal 1436   wceq 1438  wex 1660   wcel 1869  cab 2408   wne 2619  wral 2776  wrex 2777  crab 2780  wsbc 3300   cun 3435   wss 3437  c0 3762  csn 3997  cop 4003  cuni 4217   class class class wbr 4421   cdm 4851   cres 4853   wfn 5594  cfv 5599   c-bnj14 29495   w-bnj15 29499   c-bnj18 29501 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-rex 2782 This theorem is referenced by:  bnj1450  29861
 Copyright terms: Public domain W3C validator