Theorem cbvrabw 3438

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109  {cab 2707  Ⅎwnfc 2876  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3403

This theorem is referenced by:  elrabsf  3796  f1ossf1o  7082  tfis  7811  cantnflem1  9618  scottexs  9816  scott0s  9817  elmptrab  23690  bnj1534  34816  scottexf  38135  scott0f  38136  aks6d1c7lem3  42143  unitscyglem3  42158  unitscyglem4  42159  eq0rabdioph  42737  rexrabdioph  42755  rexfrabdioph  42756  elnn0rabdioph  42764  dvdsrabdioph  42771  binomcxplemdvsum  44317  fnlimcnv  45638  fnlimabslt  45650  stoweidlem34  46005  stoweidlem59  46030  pimltmnf2f  46668  pimgtpnf2f  46676  pimltpnf2f  46683  issmff  46705  smfpimltxrmptf  46729  smfpreimagtf  46739  smflim  46748  smfpimgtxr  46751  smfpimgtxrmptf  46755  smflim2  46777  smflimsup  46799  smfliminf  46802