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

Theorem ax11wdemo 1709
Description: Example of an application of ax11w 1707 that results in an instance of ax-11 1727 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 1688 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
ax11wdemo  |-  ( 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 ax11wdemo
Dummy variables  w  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elequ1 1699 . . 3  |-  ( x  =  y  ->  (
x  e.  y  <->  y  e.  y ) )
2 elequ2 1701 . . . . 5  |-  ( x  =  w  ->  (
z  e.  x  <->  z  e.  w ) )
32cbvalvw 1688 . . . 4  |-  ( A. x  z  e.  x  <->  A. w  z  e.  w
)
43a1i 10 . . 3  |-  ( x  =  y  ->  ( A. x  z  e.  x 
<-> 
A. w  z  e.  w ) )
5 elequ1 1699 . . . . . 6  |-  ( y  =  v  ->  (
y  e.  x  <->  v  e.  x ) )
65albidv 1615 . . . . 5  |-  ( y  =  v  ->  ( A. z  y  e.  x 
<-> 
A. z  v  e.  x ) )
76cbvalvw 1688 . . . 4  |-  ( A. y A. z  y  e.  x  <->  A. v A. z 
v  e.  x )
8 elequ2 1701 . . . . . 6  |-  ( x  =  y  ->  (
v  e.  x  <->  v  e.  y ) )
98albidv 1615 . . . . 5  |-  ( x  =  y  ->  ( A. z  v  e.  x 
<-> 
A. z  v  e.  y ) )
109albidv 1615 . . . 4  |-  ( x  =  y  ->  ( A. v A. z  v  e.  x  <->  A. v A. z  v  e.  y ) )
117, 10syl5bb 248 . . 3  |-  ( x  =  y  ->  ( A. y A. z  y  e.  x  <->  A. v A. z  v  e.  y ) )
121, 4, 113anbi123d 1252 . 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 1701 . . 3  |-  ( y  =  v  ->  (
x  e.  y  <->  x  e.  v ) )
147a1i 10 . . 3  |-  ( y  =  v  ->  ( A. y A. z  y  e.  x  <->  A. v A. z  v  e.  x ) )
1513, 143anbi13d 1254 . 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, 15ax11w 1707 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 set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934   A.wal 1530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1532
  Copyright terms: Public domain W3C validator