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

Theorem bnj1448 33057
 Description: Technical lemma for bnj60 33072. 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
bnj1448.1
bnj1448.2
bnj1448.3
bnj1448.4
bnj1448.5
bnj1448.6
bnj1448.7
bnj1448.8
bnj1448.9
bnj1448.10
bnj1448.11
bnj1448.12
bnj1448.13
Assertion
Ref Expression
bnj1448
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)

Proof of Theorem bnj1448
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bnj1448.12 . . . . 5
2 bnj1448.10 . . . . . . 7
3 bnj1448.9 . . . . . . . . . 10
43bnj1317 32834 . . . . . . . . 9
54nfcii 2612 . . . . . . . 8
65nfuni 4244 . . . . . . 7
72, 6nfcxfr 2620 . . . . . 6
8 nfcv 2622 . . . . . . . 8
9 nfcv 2622 . . . . . . . . 9
10 bnj1448.11 . . . . . . . . . 10
11 nfcv 2622 . . . . . . . . . . . 12
127, 11nfres 5266 . . . . . . . . . . 11
138, 12nfop 4222 . . . . . . . . . 10
1410, 13nfcxfr 2620 . . . . . . . . 9
159, 14nffv 5864 . . . . . . . 8
168, 15nfop 4222 . . . . . . 7
1716nfsn 4078 . . . . . 6
187, 17nfun 3653 . . . . 5
191, 18nfcxfr 2620 . . . 4
20 nfcv 2622 . . . 4
2119, 20nffv 5864 . . 3
22 bnj1448.13 . . . . 5
23 nfcv 2622 . . . . . . 7
2419, 23nfres 5266 . . . . . 6
2520, 24nfop 4222 . . . . 5
2622, 25nfcxfr 2620 . . . 4
279, 26nffv 5864 . . 3
2821, 27nfeq 2633 . 2
2928nfri 1817 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   w3a 968  wal 1372   wceq 1374  wex 1591   wcel 1762  cab 2445   wne 2655  wral 2807  wrex 2808  crab 2811  wsbc 3324   cun 3467   wss 3469  c0 3778  csn 4020  cop 4026  cuni 4238   class class class wbr 4440   cdm 4992   cres 4994   wfn 5574  cfv 5579   c-bnj14 32695   w-bnj15 32699   c-bnj18 32701 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-xp 4998  df-res 5004  df-iota 5542  df-fv 5587 This theorem is referenced by:  bnj1450  33060  bnj1463  33065
 Copyright terms: Public domain W3C validator