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

Metamath Proof Explorer

Theorem cbvrexfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf with a disjoint variable condition, which does not require ax-13 . For a version not dependent on ax-11 and ax-12, see cbvrexvw . (Contributed by FL, 27-Apr-2008) Avoid ax-10 , ax-13 . (Revised by GG, 10-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cbvrexfw.1 ⊢ Ⅎ 𝑥 𝐴
2 cbvrexfw.2 ⊢ Ⅎ 𝑦 𝐴
3 cbvrexfw.3 ⊢ Ⅎ 𝑦 𝜑
4 cbvrexfw.4 ⊢ Ⅎ 𝑥 𝜓
5 cbvrexfw.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6 3 nfn ⊢ Ⅎ 𝑦 ¬ 𝜑
7 4 nfn ⊢ Ⅎ 𝑥 ¬ 𝜓
8 5 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
9 1 2 6 7 8 cbvralfw ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 )
10 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝜑 )
11 ralnex ⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝜓 )
12 9 10 11 3bitr3i ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝜓 )
13 12 con4bii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 𝜓 )