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

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

Proof of Theorem bnj1371
StepHypRef Expression
1 bnj1371.9 . . . . . . 7
21bnj1436 29211 . . . . . 6
3 rexex 2765 . . . . . 6
42, 3syl 16 . . . . 5
5 bnj1371.11 . . . . . 6
65exbii 1592 . . . . 5
74, 6sylib 189 . . . 4
8 exsimpl 1602 . . . 4
97, 8syl 16 . . 3
10 bnj1371.3 . . . . . . 7
1110abeq2i 2543 . . . . . 6
1211bnj1238 29178 . . . . 5
13 fnfun 5542 . . . . 5
1412, 13bnj31 29084 . . . 4
1514bnj1265 29184 . . 3
169, 15bnj593 29113 . 2
1716bnj937 29142 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725  cab 2422   wne 2599  wral 2705  wrex 2706  crab 2709  wsbc 3161   cun 3318   wss 3320  c0 3628  csn 3814  cop 3817  cuni 4015   class class class wbr 4212   cdm 4878   cres 4880   wfun 5448   wfn 5449  cfv 5454   c-bnj14 29052   w-bnj15 29056   c-bnj18 29058 This theorem is referenced by:  bnj1384  29401 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-ral 2710  df-rex 2711  df-fn 5457
 Copyright terms: Public domain W3C validator