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

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

Proof of Theorem bnj1445
StepHypRef Expression
1 bnj1445.21 . . 3
2 bnj1445.20 . . . . . . 7
3 bnj1445.19 . . . . . . . . 9
4 bnj1445.17 . . . . . . . . . . 11
5 bnj1445.7 . . . . . . . . . . . . . . 15
6 bnj1445.6 . . . . . . . . . . . . . . . . 17
7 nfv 1609 . . . . . . . . . . . . . . . . . 18
8 bnj1445.5 . . . . . . . . . . . . . . . . . . . 20
9 bnj1445.4 . . . . . . . . . . . . . . . . . . . . . . . 24
10 bnj1445.3 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
11 nfre1 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1211nfab 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1310, 12nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1413nfcri 2426 . . . . . . . . . . . . . . . . . . . . . . . . 25
15 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . 25
1614, 15nfan 1783 . . . . . . . . . . . . . . . . . . . . . . . 24
179, 16nfxfr 1560 . . . . . . . . . . . . . . . . . . . . . . 23
1817nfex 1779 . . . . . . . . . . . . . . . . . . . . . 22
1918nfn 1777 . . . . . . . . . . . . . . . . . . . . 21
20 nfcv 2432 . . . . . . . . . . . . . . . . . . . . 21
2119, 20nfrab 2734 . . . . . . . . . . . . . . . . . . . 20
228, 21nfcxfr 2429 . . . . . . . . . . . . . . . . . . 19
23 nfcv 2432 . . . . . . . . . . . . . . . . . . 19
2422, 23nfne 2552 . . . . . . . . . . . . . . . . . 18
257, 24nfan 1783 . . . . . . . . . . . . . . . . 17
266, 25nfxfr 1560 . . . . . . . . . . . . . . . 16
2722nfcri 2426 . . . . . . . . . . . . . . . 16
28 nfv 1609 . . . . . . . . . . . . . . . . 17
2922, 28nfral 2609 . . . . . . . . . . . . . . . 16
3026, 27, 29nf3an 1786 . . . . . . . . . . . . . . 15
315, 30nfxfr 1560 . . . . . . . . . . . . . 14
3231nfri 1754 . . . . . . . . . . . . 13
3332bnj1351 29175 . . . . . . . . . . . 12
3433nfi 1541 . . . . . . . . . . 11
354, 34nfxfr 1560 . . . . . . . . . 10
36 nfv 1609 . . . . . . . . . 10
3735, 36nfan 1783 . . . . . . . . 9
383, 37nfxfr 1560 . . . . . . . 8
39 bnj1445.9 . . . . . . . . . 10
40 nfcv 2432 . . . . . . . . . . . 12
41 bnj1445.8 . . . . . . . . . . . . 13
42 nfcv 2432 . . . . . . . . . . . . . 14
4342, 17nfsbc 3025 . . . . . . . . . . . . 13
4441, 43nfxfr 1560 . . . . . . . . . . . 12
4540, 44nfrex 2611 . . . . . . . . . . 11
4645nfab 2436 . . . . . . . . . 10
4739, 46nfcxfr 2429 . . . . . . . . 9
4847nfcri 2426 . . . . . . . 8
49 nfv 1609 . . . . . . . 8
5038, 48, 49nf3an 1786 . . . . . . 7
512, 50nfxfr 1560 . . . . . 6
5251nfri 1754 . . . . 5
53 ax-17 1606 . . . . 5
5414nfri 1754 . . . . 5
55 ax-17 1606 . . . . 5
5652, 53, 54, 55bnj982 29126 . . . 4
5756nfi 1541 . . 3
581, 57nfxfr 1560 . 2
5958nfri 1754 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3a 934  wal 1530  wex 1531   wceq 1632   wcel 1696  cab 2282   wne 2459  wral 2556  wrex 2557  crab 2560  wsbc 3004   cun 3163   wss 3165  c0 3468  csn 3653  cop 3656  cuni 3843   class class class wbr 4039   cdm 4705   cres 4707   wfn 5266  cfv 5271   w-bnj17 29027   c-bnj14 29029   w-bnj15 29033   c-bnj18 29035 This theorem is referenced by:  bnj1450  29396 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-sbc 3005  df-bnj17 29028
 Copyright terms: Public domain W3C validator