Theorem ax11wdemo 1723

Description: Example of an application of ax11w 1721 that results in an instance of ax-11 1746 for a contrived formula with mixed free and bound variables, (x ∈ y ∧ ∀xz ∈ x ∧ ∀y∀zy ∈ x), in place of φ. The proof illustrates bound variable renaming with cbvalvw 1702 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
ax11wdemo	⊢ (x = y → (∀y(x ∈ y ∧ ∀x z ∈ x ∧ ∀y∀z y ∈ x) → ∀x(x = y → (x ∈ y ∧ ∀x z ∈ x ∧ ∀y∀z y ∈ x))))

Distinct variable group:   x,y,z

Proof of Theorem ax11wdemo

Dummy variables w v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elequ1 1713	. . 3 ⊢ (x = y → (x ∈ y ↔ y ∈ y))
2		elequ2 1715	. . . . 5 ⊢ (x = w → (z ∈ x ↔ z ∈ w))
3	2	cbvalvw 1702	. . . 4 ⊢ (∀x z ∈ x ↔ ∀w z ∈ w)
4	3	a1i 10	. . 3 ⊢ (x = y → (∀x z ∈ x ↔ ∀w z ∈ w))
5		elequ1 1713	. . . . . 6 ⊢ (y = v → (y ∈ x ↔ v ∈ x))
6	5	albidv 1625	. . . . 5 ⊢ (y = v → (∀z y ∈ x ↔ ∀z v ∈ x))
7	6	cbvalvw 1702	. . . 4 ⊢ (∀y∀z y ∈ x ↔ ∀v∀z v ∈ x)
8		elequ2 1715	. . . . . 6 ⊢ (x = y → (v ∈ x ↔ v ∈ y))
9	8	albidv 1625	. . . . 5 ⊢ (x = y → (∀z v ∈ x ↔ ∀z v ∈ y))
10	9	albidv 1625	. . . 4 ⊢ (x = y → (∀v∀z v ∈ x ↔ ∀v∀z v ∈ y))
11	7, 10	syl5bb 248	. . 3 ⊢ (x = y → (∀y∀z y ∈ x ↔ ∀v∀z v ∈ y))
12	1, 4, 11	3anbi123d 1252	. 2 ⊢ (x = y → ((x ∈ y ∧ ∀x z ∈ x ∧ ∀y∀z y ∈ x) ↔ (y ∈ y ∧ ∀w z ∈ w ∧ ∀v∀z v ∈ y)))
13		elequ2 1715	. . 3 ⊢ (y = v → (x ∈ y ↔ x ∈ v))
14	7	a1i 10	. . 3 ⊢ (y = v → (∀y∀z y ∈ x ↔ ∀v∀z v ∈ x))
15	13, 14	3anbi13d 1254	. 2 ⊢ (y = v → ((x ∈ y ∧ ∀x z ∈ x ∧ ∀y∀z y ∈ x) ↔ (x ∈ v ∧ ∀x z ∈ x ∧ ∀v∀z v ∈ x)))
16	12, 15	ax11w 1721	1 ⊢ (x = y → (∀y(x ∈ y ∧ ∀x z ∈ x ∧ ∀y∀z y ∈ x) → ∀x(x = y → (x ∈ y ∧ ∀x z ∈ x ∧ ∀y∀z y ∈ x))))

Syntax hints:   → wi 4   ↔ wb 176   ∧ w3a 934  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714

This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1542

This theorem is referenced by: (None)