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

Theorem ax12wdemo 1998
Description: Example of an application of ax12w 1996 that results in an instance of ax-12 2032 for a contrived formula with mixed free and bound variables, (𝑥𝑦 ∧ ∀𝑥𝑧𝑥 ∧ ∀𝑦𝑧𝑦𝑥), in place of 𝜑. The proof illustrates bound variable renaming with cbvalvw 1955 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 1983 . . 3 (𝑥 = 𝑦 → (𝑥𝑦𝑦𝑦))
2 elequ2 1990 . . . . 5 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
32cbvalvw 1955 . . . 4 (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤)
43a1i 11 . . 3 (𝑥 = 𝑦 → (∀𝑥 𝑧𝑥 ↔ ∀𝑤 𝑧𝑤))
5 elequ1 1983 . . . . . 6 (𝑦 = 𝑣 → (𝑦𝑥𝑣𝑥))
65albidv 1835 . . . . 5 (𝑦 = 𝑣 → (∀𝑧 𝑦𝑥 ↔ ∀𝑧 𝑣𝑥))
76cbvalvw 1955 . . . 4 (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥)
8 elequ2 1990 . . . . . 6 (𝑥 = 𝑦 → (𝑣𝑥𝑣𝑦))
98albidv 1835 . . . . 5 (𝑥 = 𝑦 → (∀𝑧 𝑣𝑥 ↔ ∀𝑧 𝑣𝑦))
109albidv 1835 . . . 4 (𝑥 = 𝑦 → (∀𝑣𝑧 𝑣𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
117, 10syl5bb 270 . . 3 (𝑥 = 𝑦 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑦))
121, 4, 113anbi123d 1390 . 2 (𝑥 = 𝑦 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑦𝑦 ∧ ∀𝑤 𝑧𝑤 ∧ ∀𝑣𝑧 𝑣𝑦)))
13 elequ2 1990 . . 3 (𝑦 = 𝑣 → (𝑥𝑦𝑥𝑣))
147a1i 11 . . 3 (𝑦 = 𝑣 → (∀𝑦𝑧 𝑦𝑥 ↔ ∀𝑣𝑧 𝑣𝑥))
1513, 143anbi13d 1392 . 2 (𝑦 = 𝑣 → ((𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) ↔ (𝑥𝑣 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑣𝑧 𝑣𝑥)))
1612, 15ax12w 1996 1 (𝑥 = 𝑦 → (∀𝑦(𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥) → ∀𝑥(𝑥 = 𝑦 → (𝑥𝑦 ∧ ∀𝑥 𝑧𝑥 ∧ ∀𝑦𝑧 𝑦𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  w3a 1030  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985
This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032  df-ex 1695
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator