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

Theorem ax12wdemo 2167
Description: Example of an application of ax12w 2165 that results in an instance of ax-12 2203 for a contrived formula with mixed free and bound variables, (𝑥𝑦 ∧ ∀𝑥𝑧𝑥 ∧ ∀𝑦𝑧𝑦𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 2125 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 2152 . . 3 (𝑥 = 𝑦 → (𝑥𝑦𝑦𝑦))
2 elequ2 2159 . . . . 5 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
32cbvalvw 2125 . . . 4 (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤)
43a1i 11 . . 3 (𝑥 = 𝑦 → (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤))
5 elequ1 2152 . . . . . 6 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
65albidv 2001 . . . . 5 (𝑦 = 𝑣 → (∀𝑧 𝑦𝑥 ↔ ∀𝑧 𝑣𝑥))
76cbvalvw 2125 . . . 4 (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥)
8 elequ2 2159 . . . . . 6 (𝑥 = 𝑦 → (𝑣𝑥𝑣𝑦))
98albidv 2001 . . . . 5 (𝑥 = 𝑦 → (∀𝑧 𝑣𝑥 ↔ ∀𝑧 𝑣𝑦))
109albidv 2001 . . . 4 (𝑥 = 𝑦 → (∀𝑣𝑧 𝑣𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
117, 10syl5bb 272 . . 3 (𝑥 = 𝑦 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
121, 4, 113anbi123d 1547 . 2 (𝑥 = 𝑦 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑦𝑦 ∧ ∀𝑤 𝑧𝑤 ∧ ∀𝑣𝑧 𝑣𝑦)))
13 elequ2 2159 . . 3 (𝑦 = 𝑣 → (𝑥𝑦𝑥𝑣))
147a1i 11 . . 3 (𝑦 = 𝑣 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥))
1513, 143anbi13d 1549 . 2 (𝑦 = 𝑣 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑥𝑣 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑣𝑧 𝑣𝑥)))
1612, 15ax12w 2165 1 (𝑥 = 𝑦 → (∀𝑦(𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1071  wal 1629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154
This theorem depends on definitions:  df-bi 197  df-an 383  df-3an 1073  df-ex 1853
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator