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

Theorem ax10 213
 Description: Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by Mario Carneiro, 10-Oct-2014.)
Assertion
Ref Expression
ax10
Distinct variable group:   ,,

Proof of Theorem ax10
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 wv 64 . . . . . 6
2 wv 64 . . . . . . . 8
3 wv 64 . . . . . . . 8
42, 3weqi 76 . . . . . . 7
5 weq 41 . . . . . . . 8
65, 2, 1wov 72 . . . . . . . . 9
76id 25 . . . . . . . 8
85, 2, 3, 7oveq1 99 . . . . . . 7
94, 1, 8cla4v 152 . . . . . 6
104ax4 150 . . . . . . 7
112, 10eqcomi 79 . . . . . 6
121, 9, 11eqtri 95 . . . . 5
1312alrimiv 151 . . . 4
14 wal 134 . . . . . 6
154wl 66 . . . . . 6
1614, 15wc 50 . . . . 5
173, 2weqi 76 . . . . . . 7
1817wl 66 . . . . . 6
193, 1weqi 76 . . . . . . . . 9
2019id 25 . . . . . . . 8
215, 3, 2, 20oveq1 99 . . . . . . 7
2217, 21cbv 180 . . . . . 6
2314, 18, 22ceq2 90 . . . . 5
2416, 23a1i 28 . . . 4
2513, 24mpbir 87 . . 3
26 wtru 43 . . 3