Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax9vax9 Unicode version

Theorem ax9vax9 27847
 Description: Derive ax-9 1684 (which has no distinct variable requirement) from a weaker version that requires that its two variables be distinct. The weaker version is axiom scheme B7 of [Tarski] p. 75. The hypotheses are the instances of the weaker version that we need. Neither ax-9 1684 nor ax-4 1692 (which can be derived from ax-9 1684) is used by the proof. Revised on 7-Aug-2015 to remove the dependence on ax-10 1678. See also the remarks for ax-9v 1632 and ax9 1683. This theorem does not actually use ax-9v 1632 so that other paths to ax-9 1684 can be demonstrated (such as in ax9sep 27849). Theorem ax9 1683 uses this one to make the derivation from ax-9v 1632. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 7-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
ax9vax9.a
ax9vax9.b
ax9vax9.e
ax9vax9.f
ax9vax9.i
ax9vax9.j
ax9vax9.k
ax9vax9.m
ax9vax9.p
ax9vax9.r
ax9vax9.t
ax9vax9.y
ax9vax9.z
Assertion
Ref Expression
ax9vax9
Distinct variable groups:   ,,,,,   ,,,,

Proof of Theorem ax9vax9
StepHypRef Expression
1 ax9vax9.i . . . 4
2 ax9vax9.m . . . 4
31, 2ax9lem3 27831 . . 3
41, 2ax9lem3 27831 . . 3
53, 4nsyl3 113 . 2
6 ax9vax9.z . . 3
7 ax-17 1628 . . . 4
8 ax9vax9.a . . . . . . 7
9 ax9vax9.b . . . . . . 7
10 ax9vax9.e . . . . . . 7
11 ax9vax9.f . . . . . . 7
12 ax9vax9.j . . . . . . 7
13 ax9vax9.k . . . . . . 7
14 ax9vax9.p . . . . . . 7
15 ax9vax9.r . . . . . . 7
16 ax9vax9.t . . . . . . 7
17 ax9vax9.y . . . . . . . 8
1815, 12, 1, 17ax9lem6 27834 . . . . . . 7
198, 9, 10, 11, 1, 12, 13, 2, 14, 15, 16, 18ax9lem18 27846 . . . . . 6
201, 2ax9lem7 27835 . . . . . . . . 9
211, 2ax9lem3 27831 . . . . . . . . . 10
221ax9lem1 27829 . . . . . . . . . . . . 13
23 ax-8 1623 . . . . . . . . . . . . 13
2422, 23syl 17 . . . . . . . . . . . 12
2524com12 29 . . . . . . . . . . 11
2625con3d 127 . . . . . . . . . 10
2721, 26syl 17 . . . . . . . . 9
2820, 27alimdh 1551 . . . . . . . 8
2928con3d 127 . . . . . . 7
3017, 29mpi 18 . . . . . 6
3119, 30syl6com 33 . . . . 5
3231con3i 129 . . . 4
337, 32alrimih 1553 . . 3
346, 33mt3 173 . 2
355, 34pm2.61i 158 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6  wal 1532 This theorem is referenced by:  ax9OLD  27848  ax9sep  27849 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538
 Copyright terms: Public domain W3C validator