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 ax12wlem
Description: Lemma for weak version of ax-12 . Uses only Tarski's FOL axiom
schemes. In some cases, this lemma may lead to shorter proofs than
ax12w . (Contributed by NM , 10-Apr-2017)
Ref
Expression
Hypothesis
ax12wlemw.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion
ax12wlem ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
Proof
Step
Hyp
Ref
Expression
1
ax12wlemw.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2
ax-5 ⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
3
1 2
ax12i ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )