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

Theorem ax11wdemo 1697
Description: Example of an application of ax11w 1695 that results in an instance of ax-11 1715 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 1676 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 1687 . . 3  |-  ( x  =  y  ->  (
x  e.  y  <->  y  e.  y ) )
2 elequ2 1689 . . . . 5  |-  ( x  =  w  ->  (
z  e.  x  <->  z  e.  w ) )
32cbvalvw 1676 . . . 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 1687 . . . . . 6  |-  ( y  =  v  ->  (
y  e.  x  <->  v  e.  x ) )
65albidv 1611 . . . . 5  |-  ( y  =  v  ->  ( A. z  y  e.  x 
<-> 
A. z  v  e.  x ) )
76cbvalvw 1676 . . . 4  |-  ( A. y A. z  y  e.  x  <->  A. v A. z 
v  e.  x )
8 elequ2 1689 . . . . . 6  |-  ( x  =  y  ->  (
v  e.  x  <->  v  e.  y ) )
98albidv 1611 . . . . 5  |-  ( x  =  y  ->  ( A. z  v  e.  x 
<-> 
A. z  v  e.  y ) )
109albidv 1611 . . . 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 1689 . . 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 1695 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 1527
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1529
  Copyright terms: Public domain W3C validator