Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Axiom scheme ax-7 (Equality)
alcomiw
Metamath Proof Explorer
Description: Weak version of ax-11 . See alcomw for the biconditional form.
Uses only Tarski's FOL axiom schemes. (Contributed by NM , 10-Apr-2017)
(Proof shortened by Wolf Lammen , 28-Dec-2023)
Ref
Expression
Hypothesis
alcomiw.1
⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
Assertion
alcomiw
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
Proof
Step
Hyp
Ref
Expression
1
alcomiw.1
⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
2
1
cbvalvw
⊢ ( ∀ 𝑦 𝜑 ↔ ∀ 𝑧 𝜓 )
3
2
biimpi
⊢ ( ∀ 𝑦 𝜑 → ∀ 𝑧 𝜓 )
4
3
alimi
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑧 𝜓 )
5
ax-5
⊢ ( ∀ 𝑥 ∀ 𝑧 𝜓 → ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 𝜓 )
6
1
biimprd
⊢ ( 𝑦 = 𝑧 → ( 𝜓 → 𝜑 ) )
7
6
equcoms
⊢ ( 𝑧 = 𝑦 → ( 𝜓 → 𝜑 ) )
8
7
spimvw
⊢ ( ∀ 𝑧 𝜓 → 𝜑 )
9
8
2alimi
⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 𝜓 → ∀ 𝑦 ∀ 𝑥 𝜑 )
10
4 5 9
3syl
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )