Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
Axiom scheme ax-13 (Quantified Equality)
cbv2OLD
Metamath Proof Explorer
Description: Obsolete version of cbv2 as of 10-Sep-2023. (Contributed by NM , 5-Aug-1993) (Revised by Mario Carneiro , 3-Oct-2016) Format
hypotheses to common style. (Revised by Wolf Lammen , 13-May-2018)
(New usage is discouraged.) (Proof modification is discouraged.)
Ref
Expression
Hypotheses
cbv2OLD.1
⊢ Ⅎ x φ
cbv2OLD.2
⊢ Ⅎ y φ
cbv2OLD.3
⊢ φ → Ⅎ y ψ
cbv2OLD.4
⊢ φ → Ⅎ x χ
cbv2OLD.5
⊢ φ → x = y → ψ ↔ χ
Assertion
cbv2OLD
⊢ φ → ∀ x ψ ↔ ∀ y χ
Proof
Step
Hyp
Ref
Expression
1
cbv2OLD.1
⊢ Ⅎ x φ
2
cbv2OLD.2
⊢ Ⅎ y φ
3
cbv2OLD.3
⊢ φ → Ⅎ y ψ
4
cbv2OLD.4
⊢ φ → Ⅎ x χ
5
cbv2OLD.5
⊢ φ → x = y → ψ ↔ χ
6
2
nf5ri
⊢ φ → ∀ y φ
7
1 6
alrimi
⊢ φ → ∀ x ∀ y φ
8
3
nf5rd
⊢ φ → ψ → ∀ y ψ
9
4
nf5rd
⊢ φ → χ → ∀ x χ
10
8 9 5
cbv2h
⊢ ∀ x ∀ y φ → ∀ x ψ ↔ ∀ y χ
11
7 10
syl
⊢ φ → ∀ x ψ ↔ ∀ y χ