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

Theorem bnj1445 29475
 Description: Technical lemma for bnj60 29493. 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 . 2
2 bnj1445.20 . . . . 5
3 bnj1445.19 . . . . . . 7
4 bnj1445.17 . . . . . . . . 9
5 bnj1445.7 . . . . . . . . . . . . 13
6 bnj1445.6 . . . . . . . . . . . . . . 15
7 nfv 1630 . . . . . . . . . . . . . . . 16
8 bnj1445.5 . . . . . . . . . . . . . . . . . 18
9 bnj1445.4 . . . . . . . . . . . . . . . . . . . . . 22
10 bnj1445.3 . . . . . . . . . . . . . . . . . . . . . . . . 25
11 nfre1 2764 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1211nfab 2578 . . . . . . . . . . . . . . . . . . . . . . . . 25
1310, 12nfcxfr 2571 . . . . . . . . . . . . . . . . . . . . . . . 24
1413nfcri 2568 . . . . . . . . . . . . . . . . . . . . . . 23
15 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . 23
1614, 15nfan 1847 . . . . . . . . . . . . . . . . . . . . . 22
179, 16nfxfr 1580 . . . . . . . . . . . . . . . . . . . . 21
1817nfex 1866 . . . . . . . . . . . . . . . . . . . 20
1918nfn 1812 . . . . . . . . . . . . . . . . . . 19
20 nfcv 2574 . . . . . . . . . . . . . . . . . . 19
2119, 20nfrab 2891 . . . . . . . . . . . . . . . . . 18
228, 21nfcxfr 2571 . . . . . . . . . . . . . . . . 17
23 nfcv 2574 . . . . . . . . . . . . . . . . 17
2422, 23nfne 2697 . . . . . . . . . . . . . . . 16
257, 24nfan 1847 . . . . . . . . . . . . . . 15
266, 25nfxfr 1580 . . . . . . . . . . . . . 14
2722nfcri 2568 . . . . . . . . . . . . . 14
28 nfv 1630 . . . . . . . . . . . . . . 15
2922, 28nfral 2761 . . . . . . . . . . . . . 14
3026, 27, 29nf3an 1850 . . . . . . . . . . . . 13
315, 30nfxfr 1580 . . . . . . . . . . . 12
3231nfri 1779 . . . . . . . . . . 11
3332bnj1351 29260 . . . . . . . . . 10
3433nfi 1561 . . . . . . . . 9
354, 34nfxfr 1580 . . . . . . . 8
36 nfv 1630 . . . . . . . 8
3735, 36nfan 1847 . . . . . . 7
383, 37nfxfr 1580 . . . . . 6
39 bnj1445.9 . . . . . . . 8
40 nfcv 2574 . . . . . . . . . 10
41 bnj1445.8 . . . . . . . . . . 11
42 nfcv 2574 . . . . . . . . . . . 12
4342, 17nfsbc 3184 . . . . . . . . . . 11
4441, 43nfxfr 1580 . . . . . . . . . 10
4540, 44nfrex 2763 . . . . . . . . 9
4645nfab 2578 . . . . . . . 8
4739, 46nfcxfr 2571 . . . . . . 7
4847nfcri 2568 . . . . . 6
49 nfv 1630 . . . . . 6
5038, 48, 49nf3an 1850 . . . . 5
512, 50nfxfr 1580 . . . 4
5251nfri 1779 . . 3
53 ax-17 1627 . . 3
5414nfri 1779 . . 3
55 ax-17 1627 . . 3
5652, 53, 54, 55bnj982 29211 . 2
571, 56hbxfrbi 1578 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937  wal 1550  wex 1551   wceq 1653   wcel 1726  cab 2424   wne 2601  wral 2707  wrex 2708  crab 2711  wsbc 3163   cun 3320   wss 3322  c0 3630  csn 3816  cop 3819  cuni 4017   class class class wbr 4214   cdm 4880   cres 4882   wfn 5451  cfv 5456   w-bnj17 29112   c-bnj14 29114   w-bnj15 29118   c-bnj18 29120 This theorem is referenced by:  bnj1450  29481 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419 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 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-sbc 3164  df-bnj17 29113
 Copyright terms: Public domain W3C validator