MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax12wdemo Structured version   Visualization version   GIF version

Theorem ax12wdemo 2014
Description: Example of an application of ax12w 2012 that results in an instance of ax-12 2049 for a contrived formula with mixed free and bound variables, (𝑥𝑦 ∧ ∀𝑥𝑧𝑥 ∧ ∀𝑦𝑧𝑦𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 1971 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
ax12wdemo (𝑥 = 𝑦 → (∀𝑦(𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥))))
Distinct variable group:   𝑥,𝑦,𝑧

Proof of Theorem ax12wdemo
Dummy variables 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elequ1 1999 . . 3 (𝑥 = 𝑦 → (𝑥𝑦𝑦𝑦))
2 elequ2 2006 . . . . 5 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
32cbvalvw 1971 . . . 4 (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤)
43a1i 11 . . 3 (𝑥 = 𝑦 → (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤))
5 elequ1 1999 . . . . . 6 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
65albidv 1851 . . . . 5 (𝑦 = 𝑣 → (∀𝑧 𝑦𝑥 ↔ ∀𝑧 𝑣𝑥))
76cbvalvw 1971 . . . 4 (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥)
8 elequ2 2006 . . . . . 6 (𝑥 = 𝑦 → (𝑣𝑥𝑣𝑦))
98albidv 1851 . . . . 5 (𝑥 = 𝑦 → (∀𝑧 𝑣𝑥 ↔ ∀𝑧 𝑣𝑦))
109albidv 1851 . . . 4 (𝑥 = 𝑦 → (∀𝑣𝑧 𝑣𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
117, 10syl5bb 272 . . 3 (𝑥 = 𝑦 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
121, 4, 113anbi123d 1396 . 2 (𝑥 = 𝑦 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑦𝑦 ∧ ∀𝑤 𝑧𝑤 ∧ ∀𝑣𝑧 𝑣𝑦)))
13 elequ2 2006 . . 3 (𝑦 = 𝑣 → (𝑥𝑦𝑥𝑣))
147a1i 11 . . 3 (𝑦 = 𝑣 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥))
1513, 143anbi13d 1398 . 2 (𝑦 = 𝑣 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑥𝑣 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑣𝑧 𝑣𝑥)))
1612, 15ax12w 2012 1 (𝑥 = 𝑦 → (∀𝑦(𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036  wal 1478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038  df-ex 1702
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator