This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes) Logical redundancy of ax-10 , ax-11 , ax-12 , ax-13 ax12dgen
Description: Degenerate instance of ax-12 where bundled variables x and y
have a common substitution. Uses only Tarski's FOL axiom schemes.
(Contributed by NM , 13-Apr-2017)
Ref
Expression
Assertion
ax12dgen ⊢ ( 𝑥 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑥 → 𝜑 ) ) )
Proof
Step
Hyp
Ref
Expression
1
ala1 ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑥 → 𝜑 ) )
2
1
a1i ⊢ ( 𝑥 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑥 → 𝜑 ) ) )