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	syl5bb	|- ( 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 ) ) ) )