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

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

Proof of Theorem bnj1449
StepHypRef Expression
1 bnj1449.19 . . 3
2 bnj1449.17 . . . . 5
3 bnj1449.7 . . . . . . 7
4 bnj1449.6 . . . . . . . . 9
5 nfv 1751 . . . . . . . . . 10
6 bnj1449.5 . . . . . . . . . . . 12
7 nfe1 1890 . . . . . . . . . . . . . 14
87nfn 1956 . . . . . . . . . . . . 13
9 nfcv 2584 . . . . . . . . . . . . 13
108, 9nfrab 3010 . . . . . . . . . . . 12
116, 10nfcxfr 2582 . . . . . . . . . . 11
12 nfcv 2584 . . . . . . . . . . 11
1311, 12nfne 2756 . . . . . . . . . 10
145, 13nfan 1984 . . . . . . . . 9
154, 14nfxfr 1692 . . . . . . . 8
1611nfcri 2577 . . . . . . . 8
17 nfv 1751 . . . . . . . . 9
1811, 17nfral 2811 . . . . . . . 8
1915, 16, 18nf3an 1986 . . . . . . 7
203, 19nfxfr 1692 . . . . . 6
21 nfv 1751 . . . . . 6
2220, 21nfan 1984 . . . . 5
232, 22nfxfr 1692 . . . 4
24 nfv 1751 . . . 4
2523, 24nfan 1984 . . 3
261, 25nfxfr 1692 . 2
2726nfri 1925 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982  wal 1435   wceq 1437  wex 1659   wcel 1868  cab 2407   wne 2618  wral 2775  wrex 2776  crab 2779  wsbc 3299   cun 3434   wss 3436  c0 3761  csn 3996  cop 4002  cuni 4216   class class class wbr 4420   cdm 4849   cres 4851   wfn 5592  cfv 5597   c-bnj14 29488   w-bnj15 29492   c-bnj18 29494 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-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rab 2784 This theorem is referenced by:  bnj1450  29854
 Copyright terms: Public domain W3C validator