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

Theorem ax12wdemo 2132
Description: Example of an application of ax12w 2130 that results in an instance of ax-12 2172 for a contrived formula with mixed free and bound variables, (𝑥𝑦 ∧ ∀𝑥𝑧𝑥 ∧ ∀𝑦𝑧𝑦𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 2040 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 2114 . . 3 (𝑥 = 𝑦 → (𝑥𝑦𝑦𝑦))
2 elequ2 2122 . . . . 5 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
32cbvalvw 2040 . . . 4 (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤)
43a1i 11 . . 3 (𝑥 = 𝑦 → (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤))
5 elequ1 2114 . . . . . 6 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
65albidv 1924 . . . . 5 (𝑦 = 𝑣 → (∀𝑧 𝑦𝑥 ↔ ∀𝑧 𝑣𝑥))
76cbvalvw 2040 . . . 4 (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥)
8 elequ2 2122 . . . . . 6 (𝑥 = 𝑦 → (𝑣𝑥𝑣𝑦))
98albidv 1924 . . . . 5 (𝑥 = 𝑦 → (∀𝑧 𝑣𝑥 ↔ ∀𝑧 𝑣𝑦))
109albidv 1924 . . . 4 (𝑥 = 𝑦 → (∀𝑣𝑧 𝑣𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
117, 10bitrid 283 . . 3 (𝑥 = 𝑦 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
121, 4, 113anbi123d 1437 . 2 (𝑥 = 𝑦 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑦𝑦 ∧ ∀𝑤 𝑧𝑤 ∧ ∀𝑣𝑧 𝑣𝑦)))
13 elequ2 2122 . . 3 (𝑦 = 𝑣 → (𝑥𝑦𝑥𝑣))
147a1i 11 . . 3 (𝑦 = 𝑣 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥))
1513, 143anbi13d 1439 . 2 (𝑦 = 𝑣 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑥𝑣 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑣𝑧 𝑣𝑥)))
1612, 15ax12w 2130 1 (𝑥 = 𝑦 → (∀𝑦(𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1088  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-ex 1783
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator