Theorem cbvrab 3170

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.)

Hypotheses

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

Assertion

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

Proof of Theorem cbvrab

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1829	. . . 4 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝜑)
2		cbvrab.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2744	. . . . 5 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
4		nfs1v 2424	. . . . 5 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑
5	3, 4	nfan 1815	. . . 4 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)
6		eleq1 2675	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
7		sbequ12 2096	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
8	6, 7	anbi12d 742	. . . 4 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)))
9	1, 5, 8	cbvab 2732	. . 3 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10		cbvrab.2	. . . . . 6 ⊢ Ⅎ𝑦𝐴
11	10	nfcri 2744	. . . . 5 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐴
12		cbvrab.3	. . . . . 6 ⊢ Ⅎ𝑦𝜑
13	12	nfsb 2427	. . . . 5 ⊢ Ⅎ𝑦[𝑧 / 𝑥]𝜑
14	11, 13	nfan 1815	. . . 4 ⊢ Ⅎ𝑦(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)
15		nfv 1829	. . . 4 ⊢ Ⅎ𝑧(𝑦 ∈ 𝐴 ∧ 𝜓)
16		eleq1 2675	. . . . 5 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
17		sbequ 2363	. . . . . 6 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18		cbvrab.4	. . . . . . 7 ⊢ Ⅎ𝑥𝜓
19		cbvrab.5	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
20	18, 19	sbie 2395	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
21	17, 20	syl6bb 274	. . . . 5 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓))
22	16, 21	anbi12d 742	. . . 4 ⊢ (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
23	14, 15, 22	cbvab 2732	. . 3 ⊢ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
24	9, 23	eqtri 2631	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
25		df-rab 2904	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
26		df-rab 2904	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
27	24, 25, 26	3eqtr4i 2641	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   = wceq 1474  Ⅎwnf 1698  [wsb 1866   ∈ wcel 1976  {cab 2595  Ⅎwnfc 2737  {crab 2899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904

This theorem is referenced by:  cbvrabv  3171  elrabsf  3440  tfis  6923  cantnflem1  8446  scottexs  8610  scott0s  8611  elmptrab  21382  bnj1534  29983  scottexf  32942  scott0f  32943  eq0rabdioph  36154  rexrabdioph  36172  rexfrabdioph  36173  elnn0rabdioph  36181  dvdsrabdioph  36188  binomcxplemdvsum  37372  fnlimcnv  38531  fnlimabslt  38543  stoweidlem34  38724  stoweidlem59  38749  pimltmnf2  39385  pimgtpnf2  39391  pimltpnf2  39397  issmff  39417  smfpimltxrmpt  39442  smfpreimagtf  39451  smflim  39460  smfpimgtxr  39463  smfpimgtxrmpt  39467