Theorem cbvabw 2867

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2869 with a disjoint variable condition, which does not require ax-10 2142, ax-13 2379. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Gino Giotto, 23-May-2024.)

Hypotheses

Ref	Expression
cbvabw.1	⊢ Ⅎ𝑦𝜑
cbvabw.2	⊢ Ⅎ𝑥𝜓
cbvabw.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvabw	⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvabw

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 = 𝑤
2		cbvabw.1	. . . . . . . 8 ⊢ Ⅎ𝑦𝜑
3	1, 2	nfim 1897	. . . . . . 7 ⊢ Ⅎ𝑦(𝑥 = 𝑤 → 𝜑)
4		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑦 = 𝑤
5		cbvabw.2	. . . . . . . 8 ⊢ Ⅎ𝑥𝜓
6	4, 5	nfim 1897	. . . . . . 7 ⊢ Ⅎ𝑥(𝑦 = 𝑤 → 𝜓)
7		equequ1 2032	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤))
8		cbvabw.3	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
9	7, 8	imbi12d 348	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 = 𝑤 → 𝜑) ↔ (𝑦 = 𝑤 → 𝜓)))
10	3, 6, 9	cbvalv1 2350	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝑤 → 𝜑) ↔ ∀𝑦(𝑦 = 𝑤 → 𝜓))
11	10	imbi2i 339	. . . . 5 ⊢ ((𝑤 = 𝑧 → ∀𝑥(𝑥 = 𝑤 → 𝜑)) ↔ (𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜓)))
12	11	albii 1821	. . . 4 ⊢ (∀𝑤(𝑤 = 𝑧 → ∀𝑥(𝑥 = 𝑤 → 𝜑)) ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜓)))
13		df-sb 2070	. . . 4 ⊢ ([𝑧 / 𝑥]𝜑 ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑥(𝑥 = 𝑤 → 𝜑)))
14		df-sb 2070	. . . 4 ⊢ ([𝑧 / 𝑦]𝜓 ↔ ∀𝑤(𝑤 = 𝑧 → ∀𝑦(𝑦 = 𝑤 → 𝜓)))
15	12, 13, 14	3bitr4i 306	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
16		df-clab 2777	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
17		df-clab 2777	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
18	15, 16, 17	3bitr4i 306	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
19	18	eqriv 2795	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538  Ⅎwnf 1785  [wsb 2069   ∈ wcel 2111  {cab 2776

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791

This theorem is referenced by:  cbvrabw  3437  cbvsbcw  3752  cbvrabcsfw  3869  rabsnifsb  4618  dfdmf  5729  dfrnf  5784  funfv2f  6727  abrexex2g  7647  bnj873  32306  ptrest  35056  poimirlem26  35083  poimirlem27  35084