Theorem cbvrabw 3436

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  Ⅎwnf 1785   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3402

This theorem is referenced by:  elrabsf  3788  f1ossf1o  7083  tfis  7807  cantnflem1  9610  scottexs  9811  scott0s  9812  elmptrab  23783  bnj1534  35029  scottexf  38419  scott0f  38420  aks6d1c7lem3  42552  unitscyglem3  42567  unitscyglem4  42568  eq0rabdioph  43133  rexrabdioph  43151  rexfrabdioph  43152  elnn0rabdioph  43160  dvdsrabdioph  43167  binomcxplemdvsum  44711  fnlimcnv  46025  fnlimabslt  46037  stoweidlem34  46392  stoweidlem59  46417  pimltmnf2f  47055  pimgtpnf2f  47063  pimltpnf2f  47070  issmff  47092  smfpimltxrmptf  47116  smfpreimagtf  47126  smflim  47135  smfpimgtxr  47138  smfpimgtxrmptf  47142  smflim2  47164  smflimsup  47186  smfliminf  47189