MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax12wdemo Structured version   Unicode version

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.
StepHypRef 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 ) )
32cbvalvw 1749 . . . 4  |-  ( A. x  z  e.  x  <->  A. w  z  e.  w
)
43a1i 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 ) )
65albidv 1680 . . . . 5  |-  ( y  =  v  ->  ( A. z  y  e.  x 
<-> 
A. z  v  e.  x ) )
76cbvalvw 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 ) )
98albidv 1680 . . . . 5  |-  ( x  =  y  ->  ( A. z  v  e.  x 
<-> 
A. z  v  e.  y ) )
109albidv 1680 . . . 4  |-  ( x  =  y  ->  ( A. v A. z  v  e.  x  <->  A. v A. z  v  e.  y ) )
117, 10syl5bb 257 . . 3  |-  ( x  =  y  ->  ( A. y A. z  y  e.  x  <->  A. v A. z  v  e.  y ) )
121, 4, 113anbi123d 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 ) )
147a1i 11 . . 3  |-  ( y  =  v  ->  ( A. y A. z  y  e.  x  <->  A. v A. z  v  e.  x ) )
1513, 143anbi13d 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 ) ) )
1612, 15ax12w 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 ) ) ) )
Colors of variables: wff setvar class
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)
  Copyright terms: Public domain W3C validator