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

Theorem ax12wdemo 1920
Description: Example of an application of ax12w 1918 that results in an instance of ax-12 1944 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 1889 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 1905 . . 3  |-  ( x  =  y  ->  (
x  e.  y  <->  y  e.  y ) )
2 elequ2 1912 . . . . 5  |-  ( x  =  w  ->  (
z  e.  x  <->  z  e.  w ) )
32cbvalvw 1889 . . . 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 1905 . . . . . 6  |-  ( y  =  v  ->  (
y  e.  x  <->  v  e.  x ) )
65albidv 1778 . . . . 5  |-  ( y  =  v  ->  ( A. z  y  e.  x 
<-> 
A. z  v  e.  x ) )
76cbvalvw 1889 . . . 4  |-  ( A. y A. z  y  e.  x  <->  A. v A. z 
v  e.  x )
8 elequ2 1912 . . . . . 6  |-  ( x  =  y  ->  (
v  e.  x  <->  v  e.  y ) )
98albidv 1778 . . . . 5  |-  ( x  =  y  ->  ( A. z  v  e.  x 
<-> 
A. z  v  e.  y ) )
109albidv 1778 . . . 4  |-  ( x  =  y  ->  ( A. v A. z  v  e.  x  <->  A. v A. z  v  e.  y ) )
117, 10syl5bb 265 . . 3  |-  ( x  =  y  ->  ( A. y A. z  y  e.  x  <->  A. v A. z  v  e.  y ) )
121, 4, 113anbi123d 1348 . 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 1912 . . 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 1350 . 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 1918 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 189    /\ w3a 991   A.wal 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907
This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-ex 1675
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator