Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax12w | Structured version Visualization version GIF version |
Description: Weak version of ax-12 2034 from which we can prove any ax-12 2034 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. An instance of the first hypothesis will normally require that 𝑥 and 𝑦 be distinct (unless 𝑥 does not occur in 𝜑). For an example of how the hypotheses can be eliminated when we substitute an expression without wff variables for 𝜑, see ax12wdemo 1999. (Contributed by NM, 10-Apr-2017.) |
Ref | Expression |
---|---|
ax12w.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
ax12w.2 | ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒)) |
Ref | Expression |
---|---|
ax12w | ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax12w.2 | . . 3 ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒)) | |
2 | 1 | spw 1954 | . 2 ⊢ (∀𝑦𝜑 → 𝜑) |
3 | ax12w.1 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 3 | ax12wlem 1996 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
5 | 2, 4 | syl5 33 | 1 ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: ax12wdemo 1999 |
Copyright terms: Public domain | W3C validator |