![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax12wdemo | Structured version Visualization version GIF version |
Description: Example of an application of ax12w 2131 that results in an instance of ax-12 2175 for a contrived formula with mixed free and bound variables, (𝑥 ∈ 𝑦 ∧ ∀𝑥𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧𝑦 ∈ 𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 2033 to obtain fresh variables to avoid distinct variable clashes. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 14-Apr-2017.) |
Ref | Expression |
---|---|
ax12wdemo | ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ1 2113 | . . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ↔ 𝑦 ∈ 𝑦)) | |
2 | elequ2 2121 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤)) | |
3 | 2 | cbvalvw 2033 | . . . 4 ⊢ (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤) |
4 | 3 | a1i 11 | . . 3 ⊢ (𝑥 = 𝑦 → (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤)) |
5 | elequ1 2113 | . . . . . 6 ⊢ (𝑦 = 𝑣 → (𝑦 ∈ 𝑥 ↔ 𝑣 ∈ 𝑥)) | |
6 | 5 | albidv 1918 | . . . . 5 ⊢ (𝑦 = 𝑣 → (∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑥)) |
7 | 6 | cbvalvw 2033 | . . . 4 ⊢ (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥) |
8 | elequ2 2121 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ 𝑥 ↔ 𝑣 ∈ 𝑦)) | |
9 | 8 | albidv 1918 | . . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑦)) |
10 | 9 | albidv 1918 | . . . 4 ⊢ (𝑥 = 𝑦 → (∀𝑣∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦)) |
11 | 7, 10 | bitrid 283 | . . 3 ⊢ (𝑥 = 𝑦 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦)) |
12 | 1, 4, 11 | 3anbi123d 1435 | . 2 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑦 ∧ ∀𝑤 𝑧 ∈ 𝑤 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑦))) |
13 | elequ2 2121 | . . 3 ⊢ (𝑦 = 𝑣 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑣)) | |
14 | 7 | a1i 11 | . . 3 ⊢ (𝑦 = 𝑣 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥)) |
15 | 13, 14 | 3anbi13d 1437 | . 2 ⊢ (𝑦 = 𝑣 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑣 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑥))) |
16 | 12, 15 | ax12w 2131 | 1 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1086 ∀wal 1535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 |
This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-ex 1777 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |