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

Theorem ax12wdemo 2129
Description: Example of an application of ax12w 2127 that results in an instance of ax-12 2169 for a contrived formula with mixed free and bound variables, (𝑥𝑦 ∧ ∀𝑥𝑧𝑥 ∧ ∀𝑦𝑧𝑦𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 2037 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 2111 . . 3 (𝑥 = 𝑦 → (𝑥𝑦𝑦𝑦))
2 elequ2 2119 . . . . 5 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
32cbvalvw 2037 . . . 4 (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤)
43a1i 11 . . 3 (𝑥 = 𝑦 → (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤))
5 elequ1 2111 . . . . . 6 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
65albidv 1921 . . . . 5 (𝑦 = 𝑣 → (∀𝑧 𝑦𝑥 ↔ ∀𝑧 𝑣𝑥))
76cbvalvw 2037 . . . 4 (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥)
8 elequ2 2119 . . . . . 6 (𝑥 = 𝑦 → (𝑣𝑥𝑣𝑦))
98albidv 1921 . . . . 5 (𝑥 = 𝑦 → (∀𝑧 𝑣𝑥 ↔ ∀𝑧 𝑣𝑦))
109albidv 1921 . . . 4 (𝑥 = 𝑦 → (∀𝑣𝑧 𝑣𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
117, 10bitrid 282 . . 3 (𝑥 = 𝑦 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
121, 4, 113anbi123d 1434 . 2 (𝑥 = 𝑦 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑦𝑦 ∧ ∀𝑤 𝑧𝑤 ∧ ∀𝑣𝑧 𝑣𝑦)))
13 elequ2 2119 . . 3 (𝑦 = 𝑣 → (𝑥𝑦𝑥𝑣))
147a1i 11 . . 3 (𝑦 = 𝑣 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥))
1513, 143anbi13d 1436 . 2 (𝑦 = 𝑣 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑥𝑣 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑣𝑧 𝑣𝑥)))
1612, 15ax12w 2127 1 (𝑥 = 𝑦 → (∀𝑦(𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1085  wal 1537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114
This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087  df-ex 1780
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator