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 1997 that results in an instance of ax-12 2034 for a contrived formula with mixed free and bound variables, (𝑥 ∈ 𝑦 ∧ ∀𝑥𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧𝑦 ∈ 𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 1956 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 1984 | . . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ↔ 𝑦 ∈ 𝑦)) | |
2 | elequ2 1991 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤)) | |
3 | 2 | cbvalvw 1956 | . . . 4 ⊢ (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤) |
4 | 3 | a1i 11 | . . 3 ⊢ (𝑥 = 𝑦 → (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤)) |
5 | elequ1 1984 | . . . . . 6 ⊢ (𝑦 = 𝑣 → (𝑦 ∈ 𝑥 ↔ 𝑣 ∈ 𝑥)) | |
6 | 5 | albidv 1836 | . . . . 5 ⊢ (𝑦 = 𝑣 → (∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑥)) |
7 | 6 | cbvalvw 1956 | . . . 4 ⊢ (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥) |
8 | elequ2 1991 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ 𝑥 ↔ 𝑣 ∈ 𝑦)) | |
9 | 8 | albidv 1836 | . . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑦)) |
10 | 9 | albidv 1836 | . . . 4 ⊢ (𝑥 = 𝑦 → (∀𝑣∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦)) |
11 | 7, 10 | syl5bb 271 | . . 3 ⊢ (𝑥 = 𝑦 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦)) |
12 | 1, 4, 11 | 3anbi123d 1391 | . 2 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑦 ∧ ∀𝑤 𝑧 ∈ 𝑤 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑦))) |
13 | elequ2 1991 | . . 3 ⊢ (𝑦 = 𝑣 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑣)) | |
14 | 7 | a1i 11 | . . 3 ⊢ (𝑦 = 𝑣 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥)) |
15 | 13, 14 | 3anbi13d 1393 | . 2 ⊢ (𝑦 = 𝑣 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑣 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑥))) |
16 | 12, 15 | ax12w 1997 | 1 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ w3a 1031 ∀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 ax-8 1979 ax-9 1986 |
This theorem depends on definitions: df-bi 196 df-an 385 df-3an 1033 df-ex 1696 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |