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

Metamath Proof Explorer

Theorem cbvralfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf with a disjoint variable condition, which does not require ax-10 , ax-13 . For a version not dependent on ax-11 and ax-12, see cbvralvw . (Contributed by NM, 7-Mar-2004) Avoid ax-10 , ax-13 . (Revised by GG, 23-May-2024)

Ref Expression
Hypotheses cbvralfw.1 ⊢ Ⅎ _ x A
cbvralfw.2 ⊢ Ⅎ _ y A
cbvralfw.3 ⊢ Ⅎ y φ
cbvralfw.4 ⊢ Ⅎ x ψ
cbvralfw.5 ⊢ x = y → φ ↔ ψ
Assertion cbvralfw ⊢ ∀ x ∈ A φ ↔ ∀ y ∈ A ψ

Proof

Step Hyp Ref Expression
1 cbvralfw.1 ⊢ Ⅎ _ x A
2 cbvralfw.2 ⊢ Ⅎ _ y A
3 cbvralfw.3 ⊢ Ⅎ y φ
4 cbvralfw.4 ⊢ Ⅎ x ψ
5 cbvralfw.5 ⊢ x = y → φ ↔ ψ
6 2 nfcri ⊢ Ⅎ y x ∈ A
7 6 3 nfim ⊢ Ⅎ y x ∈ A → φ
8 1 nfcri ⊢ Ⅎ x y ∈ A
9 8 4 nfim ⊢ Ⅎ x y ∈ A → ψ
10 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
11 10 5 imbi12d ⊢ x = y → x ∈ A → φ ↔ y ∈ A → ψ
12 7 9 11 cbvalv1 ⊢ ∀ x x ∈ A → φ ↔ ∀ y y ∈ A → ψ
13 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
14 df-ral ⊢ ∀ y ∈ A ψ ↔ ∀ y y ∈ A → ψ
15 12 13 14 3bitr4i ⊢ ∀ x ∈ A φ ↔ ∀ y ∈ A ψ