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

Theorem ax12w 2130
Description: Weak version of ax-12 2172 from which we can prove any ax-12 2172 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. An instance of the first hypothesis will normally require that 𝑥 and 𝑦 be distinct (unless 𝑥 does not occur in 𝜑). For an example of how the hypotheses can be eliminated when we substitute an expression without wff variables for 𝜑, see ax12wdemo 2132. (Contributed by NM, 10-Apr-2017.)
Hypotheses
Ref Expression
ax12w.1 (𝑥 = 𝑦 → (𝜑𝜓))
ax12w.2 (𝑦 = 𝑧 → (𝜑𝜒))
Assertion
Ref Expression
ax12w (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
Distinct variable groups:   𝑦,𝑧   𝜓,𝑥   𝜑,𝑧   𝜒,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦,𝑧)   𝜒(𝑥,𝑧)

Proof of Theorem ax12w
StepHypRef Expression
1 ax12w.2 . . 3 (𝑦 = 𝑧 → (𝜑𝜒))
21spw 2038 . 2 (∀𝑦𝜑𝜑)
3 ax12w.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
43ax12wlem 2129 . 2 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
52, 4syl5 34 1 (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  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
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  ax12wdemo  2132
  Copyright terms: Public domain W3C validator