Theorem ax12wdemo 2171

Description: Example of an application of ax12w 2169 that results in an instance of ax-12 2212 for a contrived formula with mixed free and bound variables, (𝑥 ∈ 𝑦 ∧ ∀𝑥𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧𝑦 ∈ 𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 2068 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 2151	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ↔ 𝑦 ∈ 𝑦))
2		elequ2 2159	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
3	2	cbvalvw 2068	. . . 4 ⊢ (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤)
4	3	a1i 11	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤))
5		elequ1 2151	. . . . . 6 ⊢ (𝑦 = 𝑣 → (𝑦 ∈ 𝑥 ↔ 𝑣 ∈ 𝑥))
6	5	albidv 1952	. . . . 5 ⊢ (𝑦 = 𝑣 → (∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑥))
7	6	cbvalvw 2068	. . . 4 ⊢ (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥)
8		elequ2 2159	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ 𝑥 ↔ 𝑣 ∈ 𝑦))
9	8	albidv 1952	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑦))
10	9	albidv 1952	. . . 4 ⊢ (𝑥 = 𝑦 → (∀𝑣∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦))
11	7, 10	bitrid 286	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦))
12	1, 4, 11	3anbi123d 1464	. 2 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑦 ∧ ∀𝑤 𝑧 ∈ 𝑤 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑦)))
13		elequ2 2159	. . 3 ⊢ (𝑦 = 𝑣 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑣))
14	7	a1i 11	. . 3 ⊢ (𝑦 = 𝑣 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥))
15	13, 14	3anbi13d 1466	. 2 ⊢ (𝑦 = 𝑣 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑣 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑥)))
16	12, 15	ax12w 2169	1 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812

This theorem is used by: (None)