This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvalv1

Description: Rule used to change bound variables, using implicit substitution. Version of cbval with a disjoint variable condition, which does not require ax-13 . See cbvalvw for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv for another variant. (Contributed by NM, 13-May-1993) (Revised by BJ, 31-May-2019)

Ref Expression
Hypotheses cbvalv1.nf1 ⊢ Ⅎ y φ
cbvalv1.nf2 ⊢ Ⅎ x ψ
cbvalv1.1 ⊢ x = y → φ ↔ ψ
Assertion cbvalv1 ⊢ ∀ x φ ↔ ∀ y ψ

Proof

Step Hyp Ref Expression
1 cbvalv1.nf1 ⊢ Ⅎ y φ
2 cbvalv1.nf2 ⊢ Ⅎ x ψ
3 cbvalv1.1 ⊢ x = y → φ ↔ ψ
4 3 biimpd ⊢ x = y → φ → ψ
5 1 2 4 cbv3v ⊢ ∀ x φ → ∀ y ψ
6 3 biimprd ⊢ x = y → ψ → φ
7 6 equcoms ⊢ y = x → ψ → φ
8 2 1 7 cbv3v ⊢ ∀ y ψ → ∀ x φ
9 5 8 impbii ⊢ ∀ x φ ↔ ∀ y ψ