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

Theorem ax11wdemoK 28275
 Description: Example of an application of ax11wK 28273 that results in an instance of ax-11 1624 for a contrived formula with mixed free and bound variables, , in place of . The proof illustrates bound variable renaming with cbvalvK 28262 to obtain fresh variables to avoid distinct variable clashes. Uses only Tarski's FOL axiom schemes (see description for equidK 28235). (Contributed by NM, 14-Apr-2017.)
Assertion
Ref Expression
ax11wdemoK
Distinct variable group:   ,,

Proof of Theorem ax11wdemoK
StepHypRef Expression
1 elequ1K 28239 . . 3
2 elequ2K 28240 . . . . 5
32cbvalvK 28262 . . . 4
43a1i 12 . . 3
5 elequ1K 28239 . . . . . 6
65albidvK 28246 . . . . 5
76cbvalvK 28262 . . . 4
8 elequ2K 28240 . . . . . 6
98albidvK 28246 . . . . 5
109albidvK 28246 . . . 4
117, 10syl5bb 250 . . 3
121, 4, 113anbi123d 1257 . 2
13 elequ2K 28240 . . 3
14 biidd 230 . . 3
157a1i 12 . . 3
1613, 14, 153anbi123d 1257 . 2
1712, 16ax11wK 28273 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178   w3a 939  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