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 -> ( A. y ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) -> A. x ( x = y -> ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) ) ) )

Proof

Step Hyp Ref Expression
1 elequ1 
 |-  ( x = y -> ( x e. y <-> y e. y ) )
2 elequ2 
 |-  ( x = w -> ( z e. x <-> z e. w ) )
3 2 cbvalvw 
 |-  ( A. x z e. x <-> A. w z e. w )
4 3 a1i 
 |-  ( x = y -> ( A. x z e. x <-> A. w z e. w ) )
5 elequ1 
 |-  ( y = v -> ( y e. x <-> v e. x ) )
6 5 albidv 
 |-  ( y = v -> ( A. z y e. x <-> A. z v e. x ) )
7 6 cbvalvw 
 |-  ( A. y A. z y e. x <-> A. v A. z v e. x )
8 elequ2 
 |-  ( x = y -> ( v e. x <-> v e. y ) )
9 8 albidv 
 |-  ( x = y -> ( A. z v e. x <-> A. z v e. y ) )
10 9 albidv 
 |-  ( x = y -> ( A. v A. z v e. x <-> A. v A. z v e. y ) )
11 7 10 bitrid 
 |-  ( x = y -> ( A. y A. z y e. x <-> A. v A. z v e. y ) )
12 1 4 11 3anbi123d 
 |-  ( x = y -> ( ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) <-> ( y e. y /\ A. w z e. w /\ A. v A. z v e. y ) ) )
13 elequ2 
 |-  ( y = v -> ( x e. y <-> x e. v ) )
14 7 a1i 
 |-  ( y = v -> ( A. y A. z y e. x <-> A. v A. z v e. x ) )
15 13 14 3anbi13d 
 |-  ( y = v -> ( ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) <-> ( x e. v /\ A. x z e. x /\ A. v A. z v e. x ) ) )
16 12 15 ax12w 
 |-  ( x = y -> ( A. y ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) -> A. x ( x = y -> ( x e. y /\ A. x z e. x /\ A. y A. z y e. x ) ) ) )