Theorem ax12wdemo 1771

Description: Example of an application of ax12w 1769 that results in an instance of ax-12 1794 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 1749 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 1761	. . 3 |- ( x = y -> ( x e. y <-> y e. y ) )
2		elequ2 1763	. . . . 5 |- ( x = w -> ( z e. x <-> z e. w ) )
3	2	cbvalvw 1749	. . . 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 1761	. . . . . 6 |- ( y = v -> ( y e. x <-> v e. x ) )
6	5	albidv 1680	. . . . 5 |- ( y = v -> ( A. z y e. x <-> A. z v e. x ) )
7	6	cbvalvw 1749	. . . 4 |- ( A. y A. z y e. x <-> A. v A. z v e. x )
8		elequ2 1763	. . . . . 6 |- ( x = y -> ( v e. x <-> v e. y ) )
9	8	albidv 1680	. . . . 5 |- ( x = y -> ( A. z v e. x <-> A. z v e. y ) )
10	9	albidv 1680	. . . 4 |- ( x = y -> ( A. v A. z v e. x <-> A. v A. z v e. y ) )
11	7, 10	syl5bb 257	. . 3 |- ( x = y -> ( A. y A. z y e. x <-> A. v A. z v e. y ) )
12	1, 4, 11	3anbi123d 1290	. 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 1763	. . 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 1292	. 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 1769	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 184   /\ w3a 965   A.wal 1368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-ex 1588

This theorem is referenced by: (None)