Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax11wdemoK Unicode version

Theorem ax11wdemoK 28155
Description: Example of an application of ax11wK 28153 that results in an instance of ax-11 1624 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 cbvalvK 28142 to obtain fresh variables to avoid distinct variable clashes. Uses only Tarski's FOL axiom schemes (see description for equidK 28115). (Contributed by NM, 14-Apr-2017.)
Assertion
Ref Expression
ax11wdemoK  |-  ( 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 ax11wdemoK
StepHypRef Expression
1 elequ1K 28119 . . 3  |-  ( x  =  y  ->  (
x  e.  y  <->  y  e.  y ) )
2 elequ2K 28120 . . . . 5  |-  ( x  =  w  ->  (
z  e.  x  <->  z  e.  w ) )
32cbvalvK 28142 . . . 4  |-  ( A. x  z  e.  x  <->  A. w  z  e.  w
)
43a1i 12 . . 3  |-  ( x  =  y  ->  ( A. x  z  e.  x 
<-> 
A. w  z  e.  w ) )
5 elequ1K 28119 . . . . . 6  |-  ( y  =  v  ->  (
y  e.  x  <->  v  e.  x ) )
65albidvK 28126 . . . . 5  |-  ( y  =  v  ->  ( A. z  y  e.  x 
<-> 
A. z  v  e.  x ) )
76cbvalvK 28142 . . . 4  |-  ( A. y A. z  y  e.  x  <->  A. v A. z 
v  e.  x )
8 elequ2K 28120 . . . . . 6  |-  ( x  =  y  ->  (
v  e.  x  <->  v  e.  y ) )
98albidvK 28126 . . . . 5  |-  ( x  =  y  ->  ( A. z  v  e.  x 
<-> 
A. z  v  e.  y ) )
109albidvK 28126 . . . 4  |-  ( x  =  y  ->  ( A. v A. z  v  e.  x  <->  A. v A. z  v  e.  y ) )
117, 10syl5bb 250 . . 3  |-  ( x  =  y  ->  ( A. y A. z  y  e.  x  <->  A. v A. z  v  e.  y ) )
121, 4, 113anbi123d 1257 . 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 elequ2K 28120 . . 3  |-  ( y  =  v  ->  (
x  e.  y  <->  x  e.  v ) )
14 biidd 230 . . 3  |-  ( y  =  v  ->  ( A. x  z  e.  x 
<-> 
A. x  z  e.  x ) )
157a1i 12 . . 3  |-  ( y  =  v  ->  ( A. y A. z  y  e.  x  <->  A. v A. z  v  e.  x ) )
1613, 14, 153anbi123d 1257 . 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 ) ) )
1712, 16ax11wK 28153 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 6    <-> wb 178    /\ w3a 939   A.wal 1532
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-8 1623  ax-13 1625  ax-14 1626  ax-17 1628  ax-9v 1632
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 941
  Copyright terms: Public domain W3C validator