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) Axiom scheme ax-7 (Equality) spfw
Description: Weak version of sp . Uses only Tarski's FOL axiom schemes. Lemma 9
of KalishMontague p. 87. This may be the best we can do with minimal
distinct variable conditions. (Contributed by NM , 19-Apr-2017) (Proof
shortened by Wolf Lammen , 10-Oct-2021)
Ref
Expression
Hypotheses
spfw.1 ⊢ ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 )
spfw.2 ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
spfw.3 ⊢ ( ¬ 𝜑 → ∀ 𝑦 ¬ 𝜑 )
spfw.4 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion
spfw ⊢ ( ∀ 𝑥 𝜑 → 𝜑 )
Proof
Step
Hyp
Ref
Expression
1
spfw.1 ⊢ ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 )
2
spfw.2 ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
3
spfw.3 ⊢ ( ¬ 𝜑 → ∀ 𝑦 ¬ 𝜑 )
4
spfw.4 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
5
4
biimpd ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
6
2 1 5
cbvaliw ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 )
7
4
biimprd ⊢ ( 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) )
8
7
equcoms ⊢ ( 𝑦 = 𝑥 → ( 𝜓 → 𝜑 ) )
9
3 8
spimw ⊢ ( ∀ 𝑦 𝜓 → 𝜑 )
10
6 9
syl ⊢ ( ∀ 𝑥 𝜑 → 𝜑 )