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 ⊢ Ⅎ 𝑥 𝐴
cbvralfw.2 ⊢ Ⅎ 𝑦 𝐴
cbvralfw.3 ⊢ Ⅎ 𝑦 𝜑
cbvralfw.4 ⊢ Ⅎ 𝑥 𝜓
cbvralfw.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion cbvralfw ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 𝜓 )

Proof

Step Hyp Ref Expression
1 cbvralfw.1 ⊢ Ⅎ 𝑥 𝐴
2 cbvralfw.2 ⊢ Ⅎ 𝑦 𝐴
3 cbvralfw.3 ⊢ Ⅎ 𝑦 𝜑
4 cbvralfw.4 ⊢ Ⅎ 𝑥 𝜓
5 cbvralfw.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6 2 nfcri ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
7 6 3 nfim ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 )
8 1 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
9 8 4 nfim ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 → 𝜓 )
10 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
11 10 5 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → 𝜓 ) ) )
12 7 9 11 cbvalv1 ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
13 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
14 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 𝜓 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
15 12 13 14 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 𝜓 )