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→∀yx∈y∧∀xz∈x∧∀y∀zy∈x→∀xx=y→x∈y∧∀xz∈x∧∀y∀zy∈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 ⊢∀xz∈x↔∀wz∈w
4 3 a1i ⊢x=y→∀xz∈x↔∀wz∈w
5 elequ1 ⊢y=v→y∈x↔v∈x
6 5 albidv ⊢y=v→∀zy∈x↔∀zv∈x
7 6 cbvalvw ⊢∀y∀zy∈x↔∀v∀zv∈x
8 elequ2 ⊢x=y→v∈x↔v∈y
9 8 albidv ⊢x=y→∀zv∈x↔∀zv∈y
10 9 albidv ⊢x=y→∀v∀zv∈x↔∀v∀zv∈y
11 7 10 bitrid ⊢x=y→∀y∀zy∈x↔∀v∀zv∈y
12 1 4 11 3anbi123d ⊢x=y→x∈y∧∀xz∈x∧∀y∀zy∈x↔y∈y∧∀wz∈w∧∀v∀zv∈y
13 elequ2 ⊢y=v→x∈y↔x∈v
14 7 a1i ⊢y=v→∀y∀zy∈x↔∀v∀zv∈x
15 13 14 3anbi13d ⊢y=v→x∈y∧∀xz∈x∧∀y∀zy∈x↔x∈v∧∀xz∈x∧∀v∀zv∈x
16 12 15 ax12w ⊢x=y→∀yx∈y∧∀xz∈x∧∀y∀zy∈x→∀xx=y→x∈y∧∀xz∈x∧∀y∀zy∈x