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

Metamath Proof Explorer

Theorem cbvrabw

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) Avoid ax-13 . (Revised by GG, 10-Jan-2024) Avoid ax-10 . (Revised by Wolf Lammen, 19-Jul-2025)

Ref Expression
Hypotheses cbvrabw.1 ⊢ Ⅎ 𝑥 𝐴
cbvrabw.2 ⊢ Ⅎ 𝑦 𝐴
cbvrabw.3 ⊢ Ⅎ 𝑦 𝜑
cbvrabw.4 ⊢ Ⅎ 𝑥 𝜓
cbvrabw.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion cbvrabw { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ 𝜓 }

Proof

Step Hyp Ref Expression
1 cbvrabw.1 ⊢ Ⅎ 𝑥 𝐴
2 cbvrabw.2 ⊢ Ⅎ 𝑦 𝐴
3 cbvrabw.3 ⊢ Ⅎ 𝑦 𝜑
4 cbvrabw.4 ⊢ Ⅎ 𝑥 𝜓
5 cbvrabw.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6 2 nfcri ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
7 6 3 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
8 1 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
9 8 4 nfan ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜓 )
10 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
11 10 5 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
12 7 9 11 cbvabw ⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) }
13 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
14 df-rab ⊢ { 𝑦 ∈ 𝐴 ∣ 𝜓 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) }
15 12 13 14 3eqtr4i ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ 𝜓 }