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	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ 𝜓 }