NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax11wdemo GIF version

Theorem ax11wdemo 1723
Description: Example of an application of ax11w 1721 that results in an instance of ax-11 1746 for a contrived formula with mixed free and bound variables, (x y xz x yzy x), in place of φ. The proof illustrates bound variable renaming with cbvalvw 1702 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 → (y(x y x z x yz y x) → x(x = y → (x y x z x yz y 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 1713 . . 3 (x = y → (x yy y))
2 elequ2 1715 . . . . 5 (x = w → (z xz w))
32cbvalvw 1702 . . . 4 (x z xw z w)
43a1i 10 . . 3 (x = y → (x z xw z w))
5 elequ1 1713 . . . . . 6 (y = v → (y xv x))
65albidv 1625 . . . . 5 (y = v → (z y xz v x))
76cbvalvw 1702 . . . 4 (yz y xvz v x)
8 elequ2 1715 . . . . . 6 (x = y → (v xv y))
98albidv 1625 . . . . 5 (x = y → (z v xz v y))
109albidv 1625 . . . 4 (x = y → (vz v xvz v y))
117, 10syl5bb 248 . . 3 (x = y → (yz y xvz v y))
121, 4, 113anbi123d 1252 . 2 (x = y → ((x y x z x yz y x) ↔ (y y w z w vz v y)))
13 elequ2 1715 . . 3 (y = v → (x yx v))
147a1i 10 . . 3 (y = v → (yz y xvz v x))
1513, 143anbi13d 1254 . 2 (y = v → ((x y x z x yz y x) ↔ (x v x z x vz v x)))
1612, 15ax11w 1721 1 (x = y → (y(x y x z x yz y x) → x(x = y → (x y x z x yz y x))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   w3a 934  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1542
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator