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

Theorem ax12f 35956
Description: Basis step for constructing a substitution instance of ax-c15 35905 without using ax-c15 35905. 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 1815 . 2 (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))
432a1i 12 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1787  ax-4 1801
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator