Axiom ax-10 1103

Description: Axiom of Quantifier Substitution. One of the equality and substitution axioms of predicate calculus with equality. Axiom scheme C11' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. This is a technical axiom wherein the antecedent is ordinarily true only if x and y are the same variable, and in that case it doesn't matter which one you use in a quantifier. (Strictly speaking, the antecedent is also true when x and y are different variables in the case of a one-element domain of discourse, but then the consequent is also true in a one-element domain. For compatibility with traditional predicate calculus all our predicate calculus axioms hold in a one-element domain, but this becomes unimportant in set theory where we show in dtru 2740 that at least 2 things exist.)

Assertion

Ref	Expression
ax-10	|- (A.x x = y -> (A.xph -> A.yph))

Detailed syntax breakdown of Axiom ax-10

Step	Hyp	Ref	Expression
1		vx	. . . . 5 set x
2	1	cv 1098	. . . 4 class x
3		vy	. . . . 5 set y
4	3	cv 1098	. . . 4 class y
5	2, 4	wceq 1099	. . 3 wff x = y
6	5, 1	wal 950	. 2 wff A.x x = y
7		wph	. . . 4 wff ph
8	7, 1	wal 950	. . 3 wff A.xph
9	7, 3	wal 950	. . 3 wff A.yph
10	8, 9	wi 3	. 2 wff (A.xph -> A.yph)
11	6, 10	wi 3	1 wff (A.x x = y -> (A.xph -> A.yph))

This axiom is referenced by:  alequcom 1125  hbae 1128  dvelimfALT 1136  dral1 1137  hbsb4 1232  a12stdy1 1349  a12stdy2 1350  a12stdy4 1352  hbeu 1366  nd1 4861  nd2 4862  axpowndlem3 4874

Copyright terms: Public domain