 Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax12f Structured version   Visualization version   GIF version

Theorem ax12f 34953
 Description: Basis step for constructing a substitution instance of ax-c15 34902 without using ax-c15 34902. We can start with any formula 𝜑 in which 𝑥 is not free. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
ax12f.1 (𝜑 → ∀𝑥𝜑)
Assertion
Ref Expression
ax12f (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))

Proof of Theorem ax12f
StepHypRef Expression
1 ax12f.1 . . 3 (𝜑 → ∀𝑥𝜑)
2 ax-1 6 . . 3 (𝜑 → (𝑥 = 𝑦𝜑))
31, 2alrimih 1919 . 2 (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))
432a1i 12 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1651 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1891  ax-4 1905 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator