Theorem cbvrabw 3449

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3453 with a disjoint variable condition, which does not require ax-13 2403. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2403. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2175. (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 2916	. . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
3		cbvrabw.3	. . . 4 ⊢ Ⅎ𝑦𝜑
4	2, 3	nfan 1919	. . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ∧ 𝜑)
5		cbvrabw.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
6	5	nfcri 2916	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
7		cbvrabw.4	. . . 4 ⊢ Ⅎ𝑥𝜓
8	6, 7	nfan 1919	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜓)
9		eleq1w 2845	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
10		cbvrabw.5	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
11	9, 10	anbi12d 641	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
12	4, 8, 11	cbvabw 2833	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
13		df-rab 3415	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
14		df-rab 3415	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
15	12, 13, 14	3eqtr4i 2795	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560  Ⅎwnf 1803   ∈ wcel 2142  {cab 2740  Ⅎwnfc 2909  {crab 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3415

This theorem is referenced by:  elrabsf  3789  f1ossf1o  7110  tfis  7835  cantnflem1  9644  scottexs  9845  scott0s  9846  elmptrab  23884  bnj1534  35145  scottexf  38664  scott0f  38665  aks6d1c7lem3  42796  unitscyglem3  42811  unitscyglem4  42812  eq0rabdioph  43354  rexrabdioph  43368  rexfrabdioph  43369  elnn0rabdioph  43377  dvdsrabdioph  43384  binomcxplemdvsum  44928  fnlimcnv  46238  fnlimabslt  46250  stoweidlem34  46605  stoweidlem59  46630  pimltmnf2f  47268  pimgtpnf2f  47276  pimltpnf2f  47283  issmff  47305  smfpimltxrmptf  47329  smfpreimagtf  47339  smflim  47348  smfpimgtxr  47351  smfpimgtxrmptf  47355  smflim2  47377  smflimsup  47399  smfliminf  47402