Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Axiom scheme ax-7 (Equality)
alcomw
Metamath Proof Explorer
Description: Weak version of alcom and biconditional form of alcomimw . Uses
only Tarski's FOL axiom schemes. (Contributed by BTernaryTau , 28-Dec-2024)
Ref
Expression
Hypotheses
alcomw.1
⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜓 ) )
alcomw.2
⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜒 ) )
Assertion
alcomw
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 𝜑 )
Proof
Step
Hyp
Ref
Expression
1
alcomw.1
⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜓 ) )
2
alcomw.2
⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜒 ) )
3
2
alcomimw
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
4
1
alcomimw
⊢ ( ∀ 𝑦 ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜑 )
5
3 4
impbii
⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 𝜑 )