Theorem cbvrabw 3447

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

Hypotheses

Ref	Expression
cbvrabw.1	⊢ Ⅎ𝑥𝐴
cbvrabw.2	⊢ Ⅎ𝑦𝐴
cbvrabw.3	⊢ Ⅎ𝑦𝜑
cbvrabw.4	⊢ Ⅎ𝑥𝜓
cbvrabw.5	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrabw	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑥, 𝑦)   𝐴(𝑥, 𝑦)

Proof of Theorem cbvrabw

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  {cab 2739  Ⅎwnfc 2908  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3414

This theorem is used by:  elrabsf  3784  f1ossf1o  7127  tfis  7864  cantnflem1  9683  scottexsOLD  9936  scott0bsOLD  9938  elmptrab  24139  bnj1534  35476  scottexf  39080  scott0f  39081  aks6d1c7lem3  43212  unitscyglem3  43227  unitscyglem4  43228  eq0rabdioph  43766  rexrabdioph  43780  rexfrabdioph  43781  elnn0rabdioph  43789  dvdsrabdioph  43796  binomcxplemdvsum  45324  fnlimcnv  46646  fnlimabslt  46658  stoweidlem34  47013  stoweidlem59  47038  pimltmnf2f  47676  pimgtpnf2f  47684  pimltpnf2f  47691  issmff  47713  smfpimltxrmptf  47737  smfpreimagtf  47747  smflim  47756  smfpimgtxr  47759  smfpimgtxrmptf  47763  smflim2  47785  smflimsup  47807  smfliminf  47810