Mathbox for Andrew Salmon < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax10ext Structured version   Unicode version

Theorem ax10ext 27574
 Description: This theorem shows that, given axext4 2419, we can derive a version of ax10 2025. However, it is weaker than ax10 2025 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.)
Assertion
Ref Expression
ax10ext
Distinct variable group:   ,

Proof of Theorem ax10ext
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax-ext 2416 . . . . . 6
21alimi 1568 . . . . 5
3 ax-7 1749 . . . . . . 7
4 ax-14 1729 . . . . . . . . 9
5 bi2 190 . . . . . . . . . . 11
65alimi 1568 . . . . . . . . . 10
7 nfv 1629 . . . . . . . . . . 11
87stdpc5 1816 . . . . . . . . . 10
96, 8syl 16 . . . . . . . . 9
104, 9syl9 68 . . . . . . . 8
1110alimdv 1631 . . . . . . 7
123, 11syl5 30 . . . . . 6
1312sps 1770 . . . . 5
142, 13mpcom 34 . . . 4
1514a5i 1807 . . 3
16 nfa1 1806 . . . . . . . 8
171619.23 1819 . . . . . . 7
18 19.8a 1762 . . . . . . . . 9
19 elequ2 1730 . . . . . . . . . 10
2019cbvexv 1985 . . . . . . . . 9
2118, 20sylib 189 . . . . . . . 8
22 nfv 1629 . . . . . . . . 9
2322, 7, 4cbv3 1971 . . . . . . . 8
2421, 23imim12i 55 . . . . . . 7
2517, 24sylbi 188 . . . . . 6
2625alimi 1568 . . . . 5
2726a7s 1750 . . . 4
2827alrimiv 1641 . . 3
29 nfa1 1806 . . . . . . . 8
302919.23 1819 . . . . . . 7
31 ax-14 1729 . . . . . . . . . 10
3231spimv 1963 . . . . . . . . 9
3318, 32imim12i 55 . . . . . . . 8
34 19.8a 1762 . . . . . . . . . 10
35 elequ2 1730 . . . . . . . . . . 11
3635cbvexv 1985 . . . . . . . . . 10
3734, 36sylib 189 . . . . . . . . 9
38 sp 1763 . . . . . . . . 9
3937, 38imim12i 55 . . . . . . . 8
4033, 39impbid 184 . . . . . . 7
4130, 40sylbi 188 . . . . . 6
4241alimi 1568 . . . . 5
4342a7s 1750 . . . 4
4443a5i 1807 . . 3
4515, 28, 443syl 19 . 2
46 axext4 2419 . . 3
4746albii 1575 . 2
48 axext4 2419 . . 3
4948albii 1575 . 2
5045, 47, 493imtr4i 258 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wal 1549  wex 1550   wceq 1652   wcel 1725 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-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554
 Copyright terms: Public domain W3C validator