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

Theorem bnj1449 29591
 Description: Technical lemma for bnj60 29605. 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 1631 . . . . . . . . . 10
6 bnj1449.5 . . . . . . . . . . . 12
7 nfe1 1750 . . . . . . . . . . . . . 14
87nfn 1814 . . . . . . . . . . . . 13
9 nfcv 2579 . . . . . . . . . . . . 13
108, 9nfrab 2896 . . . . . . . . . . . 12
116, 10nfcxfr 2576 . . . . . . . . . . 11
12 nfcv 2579 . . . . . . . . . . 11
1311, 12nfne 2702 . . . . . . . . . 10
145, 13nfan 1849 . . . . . . . . 9
154, 14nfxfr 1580 . . . . . . . 8
1611nfcri 2573 . . . . . . . 8
17 nfv 1631 . . . . . . . . 9
1811, 17nfral 2766 . . . . . . . 8
1915, 16, 18nf3an 1852 . . . . . . 7
203, 19nfxfr 1580 . . . . . 6
21 nfv 1631 . . . . . 6
2220, 21nfan 1849 . . . . 5
232, 22nfxfr 1580 . . . 4
24 nfv 1631 . . . 4
2523, 24nfan 1849 . . 3
261, 25nfxfr 1580 . 2
2726nfri 1781 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937  wal 1550  wex 1551   wceq 1654   wcel 1728  cab 2429   wne 2606  wral 2712  wrex 2713  crab 2716  wsbc 3170   cun 3307   wss 3309  c0 3616  csn 3843  cop 3846  cuni 4044   class class class wbr 4243   cdm 4913   cres 4915   wfn 5484  cfv 5489   c-bnj14 29226   w-bnj15 29230   c-bnj18 29232 This theorem is referenced by:  bnj1450  29593 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rab 2721
 Copyright terms: Public domain W3C validator