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

Metamath Proof Explorer

Theorem cbvmow

Description: Rule used to change bound variables, using implicit substitution. Version of cbvmo with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 9-Mar-1995) (Revised by GG, 23-May-2024)

Ref Expression
Hypotheses cbvmow.1 ⊢ Ⅎ 𝑦 𝜑
cbvmow.2 ⊢ Ⅎ 𝑥 𝜓
cbvmow.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion cbvmow ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 cbvmow.1 ⊢ Ⅎ 𝑦 𝜑
2 cbvmow.2 ⊢ Ⅎ 𝑥 𝜓
3 cbvmow.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4 nfv ⊢ Ⅎ 𝑦 𝑥 = 𝑧
5 1 4 nfim ⊢ Ⅎ 𝑦 ( 𝜑 → 𝑥 = 𝑧 )
6 nfv ⊢ Ⅎ 𝑥 𝑦 = 𝑧
7 2 6 nfim ⊢ Ⅎ 𝑥 ( 𝜓 → 𝑦 = 𝑧 )
8 equequ1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )
9 3 8 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → 𝑥 = 𝑧 ) ↔ ( 𝜓 → 𝑦 = 𝑧 ) ) )
10 5 7 9 cbvalv1 ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
11 10 exbii ⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
12 df-mo ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) )
13 df-mo ⊢ ( ∃* 𝑦 𝜓 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
14 11 12 13 3bitr4i ⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )