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

Metamath Proof Explorer

Theorem cbvrmow

Description: Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 16-Jun-2017) Avoid ax-10 , ax-13 . (Revised by GG, 23-May-2024)

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

Proof

Step Hyp Ref Expression
1 cbvrmow.1 ⊢ Ⅎ 𝑦 𝜑
2 cbvrmow.2 ⊢ Ⅎ 𝑥 𝜓
3 cbvrmow.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
5 4 1 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
6 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
7 6 2 nfan ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜓 )
8 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
9 8 3 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
10 5 7 9 cbvmow ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
11 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
12 df-rmo ⊢ ( ∃* 𝑦 ∈ 𝐴 𝜓 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
13 10 11 12 3bitr4i ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∈ 𝐴 𝜓 )