Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-c10 | Structured version Visualization version GIF version |
Description: A variant of ax6 2385.
Axiom scheme C10' in [Megill] p. 448 (p. 16 of
the
preprint).
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc10 2386. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-c10 | ⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . . . 5 setvar 𝑥 | |
2 | vy | . . . . 5 setvar 𝑦 | |
3 | 1, 2 | weq 1969 | . . . 4 wff 𝑥 = 𝑦 |
4 | wph | . . . . 5 wff 𝜑 | |
5 | 4, 1 | wal 1539 | . . . 4 wff ∀𝑥𝜑 |
6 | 3, 5 | wi 4 | . . 3 wff (𝑥 = 𝑦 → ∀𝑥𝜑) |
7 | 6, 1 | wal 1539 | . 2 wff ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) |
8 | 7, 4 | wi 4 | 1 wff (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) |
Colors of variables: wff setvar class |
This axiom is referenced by: ax6fromc10 36889 equid1 36892 equid1ALT 36918 |
Copyright terms: Public domain | W3C validator |