HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax10 Unicode version

Theorem ax10 200
Description: Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).
Assertion
Ref Expression
ax10 |- T. |= [(A.\x:al [x:al = y:al]) ==> (A.\y:al [y:al = x:al])]
Distinct variable group:   x,y,al

Proof of Theorem ax10
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 wv 58 . . . . . 6 |- z:al:al
2 wv 58 . . . . . . . 8 |- x:al:al
3 wv 58 . . . . . . . 8 |- y:al:al
42, 3weqi 68 . . . . . . 7 |- [x:al = y:al]:*
5 weq 38 . . . . . . . 8 |- = :(al -> (al -> *))
65, 2, 1wov 64 . . . . . . . . 9 |- [x:al = z:al]:*
76id 25 . . . . . . . 8 |- [x:al = z:al] |= [x:al = z:al]
85, 2, 3, 7oveq1 89 . . . . . . 7 |- [x:al = z:al] |= [[x:al = y:al] = [z:al = y:al]]
94, 1, 8cla4v 142 . . . . . 6 |- (A.\x:al [x:al = y:al]) |= [z:al = y:al]
104ax4 140 . . . . . . 7 |- (A.\x:al [x:al = y:al]) |= [x:al = y:al]
112, 10eqcomi 70 . . . . . 6 |- (A.\x:al [x:al = y:al]) |= [y:al = x:al]
121, 9, 11eqtri 85 . . . . 5 |- (A.\x:al [x:al = y:al]) |= [z:al = x:al]
1312alrimiv 141 . . . 4 |- (A.\x:al [x:al = y:al]) |= (A.\z:al [z:al = x:al])
14 wal 124 . . . . . 6 |- A.:((al -> *) -> *)
154wl 59 . . . . . 6 |- \x:al [x:al = y:al]:(al -> *)
1614, 15wc 45 . . . . 5 |- (A.\x:al [x:al = y:al]):*
173, 2weqi 68 . . . . . . 7 |- [y:al = x:al]:*
1817wl 59 . . . . . 6 |- \y:al [y:al = x:al]:(al -> *)
193, 1weqi 68 . . . . . . . . 9 |- [y:al = z:al]:*
2019id 25 . . . . . . . 8 |- [y:al = z:al] |= [y:al = z:al]
215, 3, 2, 20oveq1 89 . . . . . . 7 |- [y:al = z:al] |= [[y:al = x:al] = [z:al = x:al]]
2217, 21cbv 168 . . . . . 6 |- T. |= [\y:al [y:al = x:al] = \z:al [z:al = x:al]]
2314, 18, 22ceq2 80 . . . . 5 |- T. |= [(A.\y:al [y:al = x:al]) = (A.\z:al [z:al = x:al])]
2416, 23a1i 28 . . . 4 |- (A.\x:al [x:al = y:al]) |= [(A.\y:al [y:al = x:al]) = (A.\z:al [z:al = x:al])]
2513, 24mpbir 77 . . 3 |- (A.\x:al [x:al = y:al]) |= (A.\y:al [y:al = x:al])
26 wtru 40 . . 3 |- T.:*
2725, 26adantl 51 . 2 |- (T., (A.\x:al [x:al = y:al])) |= (A.\y:al [y:al = x:al])
2827ex 148 1 |- T. |= [(A.\x:al [x:al = y:al]) ==> (A.\y:al [y:al = x:al])]
Colors of variables: type var term
Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9   |= wffMMJ2 11   ==> tim 111  A.tal 112
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103  ax-eta 165
This theorem depends on definitions:  df-ov 65  df-al 116  df-an 118  df-im 119
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator