Theorem ax12wdemo 2129

Description: Example of an application of ax12w 2127 that results in an instance of ax-12 2163 for a contrived formula with mixed free and bound variables, (𝑥 ∈ 𝑦 ∧ ∀𝑥𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧𝑦 ∈ 𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 2086 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 2114	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ↔ 𝑦 ∈ 𝑦))
2		elequ2 2121	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
3	2	cbvalvw 2086	. . . 4 ⊢ (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤)
4	3	a1i 11	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑥 𝑧 ∈ 𝑥 ↔ ∀𝑤 𝑧 ∈ 𝑤))
5		elequ1 2114	. . . . . 6 ⊢ (𝑦 = 𝑣 → (𝑦 ∈ 𝑥 ↔ 𝑣 ∈ 𝑥))
6	5	albidv 1963	. . . . 5 ⊢ (𝑦 = 𝑣 → (∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑥))
7	6	cbvalvw 2086	. . . 4 ⊢ (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥)
8		elequ2 2121	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑣 ∈ 𝑥 ↔ 𝑣 ∈ 𝑦))
9	8	albidv 1963	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑧 𝑣 ∈ 𝑦))
10	9	albidv 1963	. . . 4 ⊢ (𝑥 = 𝑦 → (∀𝑣∀𝑧 𝑣 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦))
11	7, 10	syl5bb 275	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑦))
12	1, 4, 11	3anbi123d 1509	. 2 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑦 ∈ 𝑦 ∧ ∀𝑤 𝑧 ∈ 𝑤 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑦)))
13		elequ2 2121	. . 3 ⊢ (𝑦 = 𝑣 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑣))
14	7	a1i 11	. . 3 ⊢ (𝑦 = 𝑣 → (∀𝑦∀𝑧 𝑦 ∈ 𝑥 ↔ ∀𝑣∀𝑧 𝑣 ∈ 𝑥))
15	13, 14	3anbi13d 1511	. 2 ⊢ (𝑦 = 𝑣 → ((𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑣 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑣∀𝑧 𝑣 ∈ 𝑥)))
16	12, 15	ax12w 2127	1 ⊢ (𝑥 = 𝑦 → (∀𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥 ∈ 𝑦 ∧ ∀𝑥 𝑧 ∈ 𝑥 ∧ ∀𝑦∀𝑧 𝑦 ∈ 𝑥))))

Syntax hints:   → wi 4   ↔ wb 198   ∧ w3a 1071  ∀wal 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116

This theorem depends on definitions:  df-bi 199  df-an 387  df-3an 1073  df-ex 1824

This theorem is referenced by: (None)