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) Equality predicate (continued) speimfw
Description: Specialization, with additional weakening (compared to 19.2 ) to allow
bundling of x and y . Uses only Tarski's FOL axiom schemes.
(Contributed by NM , 23-Apr-2017) (Proof shortened by Wolf Lammen , 5-Dec-2017)
Ref
Expression
Hypothesis
speimfw.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
Assertion
speimfw ⊢ ( ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
speimfw.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
2
df-ex ⊢ ( ∃ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 )
3
2
biimpri ⊢ ( ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 → ∃ 𝑥 𝑥 = 𝑦 )
4
1
com12 ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → 𝜓 ) )
5
4
aleximi ⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝜓 ) )
6
3 5
syl5com ⊢ ( ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )