This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax12wdemo

Description: Example of an application of ax12w that results in an instance of ax-12 for a contrived formula with mixed free and bound variables, ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) , in place of ph . The proof illustrates bound variable renaming with cbvalvw to obtain fresh variables to avoid distinct variable clashes. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 14-Apr-2017)

Ref Expression
Assertion ax12wdemo ⊢ x = y → ∀ y x ∈ y ∧ ∀ x z ∈ x ∧ ∀ y ∀ z y ∈ x → ∀ x x = y → x ∈ y ∧ ∀ x z ∈ x ∧ ∀ y ∀ z y ∈ x

Proof

Step Hyp Ref Expression
1 elequ1 ⊢ x = y → x ∈ y ↔ y ∈ y
2 elequ2 ⊢ x = w → z ∈ x ↔ z ∈ w
3 2 cbvalvw ⊢ ∀ x z ∈ x ↔ ∀ w z ∈ w
4 3 a1i ⊢ x = y → ∀ x z ∈ x ↔ ∀ w z ∈ w
5 elequ1 ⊢ y = v → y ∈ x ↔ v ∈ x
6 5 albidv ⊢ y = v → ∀ z y ∈ x ↔ ∀ z v ∈ x
7 6 cbvalvw ⊢ ∀ y ∀ z y ∈ x ↔ ∀ v ∀ z v ∈ x
8 elequ2 ⊢ x = y → v ∈ x ↔ v ∈ y
9 8 albidv ⊢ x = y → ∀ z v ∈ x ↔ ∀ z v ∈ y
10 9 albidv ⊢ x = y → ∀ v ∀ z v ∈ x ↔ ∀ v ∀ z v ∈ y
11 7 10 bitrid ⊢ x = y → ∀ y ∀ z y ∈ x ↔ ∀ v ∀ z v ∈ y
12 1 4 11 3anbi123d ⊢ x = y → x ∈ y ∧ ∀ x z ∈ x ∧ ∀ y ∀ z y ∈ x ↔ y ∈ y ∧ ∀ w z ∈ w ∧ ∀ v ∀ z v ∈ y
13 elequ2 ⊢ y = v → x ∈ y ↔ x ∈ v
14 7 a1i ⊢ y = v → ∀ y ∀ z y ∈ x ↔ ∀ v ∀ z v ∈ x
15 13 14 3anbi13d ⊢ y = v → x ∈ y ∧ ∀ x z ∈ x ∧ ∀ y ∀ z y ∈ x ↔ x ∈ v ∧ ∀ x z ∈ x ∧ ∀ v ∀ z v ∈ x
16 12 15 ax12w ⊢ x = y → ∀ y x ∈ y ∧ ∀ x z ∈ x ∧ ∀ y ∀ z y ∈ x → ∀ x x = y → x ∈ y ∧ ∀ x z ∈ x ∧ ∀ y ∀ z y ∈ x