Theorem ax12wdemo 1881

Description: Example of an application of ax12w 1879 that results in an instance of ax-12 1905 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 1859 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
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 ) ) ) )

Distinct variable group:   x, y, z

Proof of Theorem ax12wdemo

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

Step	Hyp	Ref	Expression
1		elequ1 1871	. . 3 |- ( x = y -> ( x e. y <-> y e. y ) )
2		elequ2 1873	. . . . 5 |- ( x = w -> ( z e. x <-> z e. w ) )
3	2	cbvalvw 1859	. . . 4 |- ( A. x z e. x <-> A. w z e. w )
4	3	a1i 11	. . 3 |- ( x = y -> ( A. x z e. x <-> A. w z e. w ) )
5		elequ1 1871	. . . . . 6 |- ( y = v -> ( y e. x <-> v e. x ) )
6	5	albidv 1757	. . . . 5 |- ( y = v -> ( A. z y e. x <-> A. z v e. x ) )
7	6	cbvalvw 1859	. . . 4 |- ( A. y A. z y e. x <-> A. v A. z v e. x )
8		elequ2 1873	. . . . . 6 |- ( x = y -> ( v e. x <-> v e. y ) )
9	8	albidv 1757	. . . . 5 |- ( x = y -> ( A. z v e. x <-> A. z v e. y ) )
10	9	albidv 1757	. . . 4 |- ( x = y -> ( A. v A. z v e. x <-> A. v A. z v e. y ) )
11	7, 10	syl5bb 260	. . 3 |- ( x = y -> ( A. y A. z y e. x <-> A. v A. z v e. y ) )
12	1, 4, 11	3anbi123d 1335	. 2 |- ( 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 1873	. . 3 |- ( y = v -> ( x e. y <-> x e. v ) )
14	7	a1i 11	. . 3 |- ( y = v -> ( A. y A. z y e. x <-> A. v A. z v e. x ) )
15	13, 14	3anbi13d 1337	. 2 |- ( 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 1879	1 |- ( 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 ) ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ w3a 982   A.wal 1435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-ex 1660

This theorem is referenced by: (None)