Theorem ax12wdemo 1959

Description: Example of an application of ax12w 1957 that results in an instance of ax-12 1983 for a contrived formula with mixed free and bound variables, (𝑥 ∈ 𝑦 ∧ ∀𝑥𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧𝑦 ∈ 𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 1917 to obtain fresh variables to avoid distinct variable clashes. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 14-Apr-2017.)

Assertion

Ref	Expression
ax12wdemo	⊢ (𝑥 = 𝑦 → (∀𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥))))

Distinct variable group:   𝑥,𝑦,𝑧

Proof of Theorem ax12wdemo

Dummy variables 𝑤 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elequ1 1944	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ↔ 𝑦 ∈ 𝑦))
2		elequ2 1951	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
3	2	cbvalvw 1917	. . . 4 ⊢ (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤)
4	3	a1i 11	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤))
5		elequ1 1944	. . . . . 6 ⊢ (𝑦 = 𝑣 → (𝑦 ∈ 𝑥 ↔ 𝑣 ∈ 𝑥))
6	5	albidv 1798	. . . . 5 ⊢ (𝑦 = 𝑣 → (∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑥))
7	6	cbvalvw 1917	. . . 4 ⊢ (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥)
8		elequ2 1951	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ 𝑥 ↔ 𝑣 ∈ 𝑦))
9	8	albidv 1798	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑦))
10	9	albidv 1798	. . . 4 ⊢ (𝑥 = 𝑦 → (∀𝑣∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦))
11	7, 10	syl5bb 267	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦))
12	1, 4, 11	3anbi123d 1381	. 2 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑦 ∧ ∀𝑤 𝑧 ∈ 𝑤 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑦)))
13		elequ2 1951	. . 3 ⊢ (𝑦 = 𝑣 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑣))
14	7	a1i 11	. . 3 ⊢ (𝑦 = 𝑣 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥))
15	13, 14	3anbi13d 1383	. 2 ⊢ (𝑦 = 𝑣 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑣 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑥)))
16	12, 15	ax12w 1957	1 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥))))

Syntax hints:   → wi 4   ↔ wb 191   ∧ w3a 1021  ∀wal 1466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946

This theorem depends on definitions:  df-bi 192  df-an 380  df-3an 1023  df-ex 1693

This theorem is referenced by: (None)