Theorem cbvrabw 3446

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3449 with a disjoint variable condition, which does not require ax-13 2401. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2401. (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 2914	. . . 4 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
3		cbvrabw.3	. . . 4 ⊢ Ⅎ𝑦𝜑
4	2, 3	nfan 1932	. . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ∧ 𝜑)
5		cbvrabw.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
6	5	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
7		cbvrabw.4	. . . 4 ⊢ Ⅎ𝑥𝜓
8	6, 7	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜓)
9		eleq1w 2843	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
10		cbvrabw.5	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
11	9, 10	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
12	4, 8, 11	cbvabw 2831	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
13		df-rab 3413	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
14		df-rab 3413	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
15	12, 13, 14	3eqtr4i 2793	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413

This theorem is used by:  elrabsf  3784  f1ossf1o  7122  tfis  7851  cantnflem1  9668  scottexsOLD  9882  scott0bsOLD  9884  elmptrab  24053  bnj1534  35362  scottexf  38916  scott0f  38917  aks6d1c7lem3  43048  unitscyglem3  43063  unitscyglem4  43064  eq0rabdioph  43621  rexrabdioph  43635  rexfrabdioph  43636  elnn0rabdioph  43644  dvdsrabdioph  43651  binomcxplemdvsum  45179  fnlimcnv  46495  fnlimabslt  46507  stoweidlem34  46862  stoweidlem59  46887  pimltmnf2f  47525  pimgtpnf2f  47533  pimltpnf2f  47540  issmff  47562  smfpimltxrmptf  47586  smfpreimagtf  47596  smflim  47605  smfpimgtxr  47608  smfpimgtxrmptf  47612  smflim2  47634  smflimsup  47656  smfliminf  47659