Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
Axiom scheme ax-13 (Quantified Equality)
cbvalvOLD
Metamath Proof Explorer
Description: Obsolete version of cbvalv as of 11-Sep-2023. (Contributed by NM , 5-Aug-1993) Remove dependency on ax-10 . (Revised by Wolf Lammen , 17-Jul-2021) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypothesis
cbvalv.1
⊢ x = y → φ ↔ ψ
Assertion
cbvalvOLD
⊢ ∀ x φ ↔ ∀ y ψ
Proof
Step
Hyp
Ref
Expression
1
cbvalv.1
⊢ x = y → φ ↔ ψ
2
ax-5
⊢ φ → ∀ y φ
3
2
hbal
⊢ ∀ x φ → ∀ y ∀ x φ
4
1
spv
⊢ ∀ x φ → ψ
5
3 4
alrimih
⊢ ∀ x φ → ∀ y ψ
6
ax-5
⊢ ψ → ∀ x ψ
7
6
hbal
⊢ ∀ y ψ → ∀ x ∀ y ψ
8
1
equcoms
⊢ y = x → φ ↔ ψ
9
8
bicomd
⊢ y = x → ψ ↔ φ
10
9
spv
⊢ ∀ y ψ → φ
11
7 10
alrimih
⊢ ∀ y ψ → ∀ x φ
12
5 11
impbii
⊢ ∀ x φ ↔ ∀ y ψ