Theorem sb8iota 5775

Description: Variable substitution in description binder. Compare sb8eu 2491. (Contributed by NM, 18-Mar-2013.)

Hypothesis

Ref	Expression
sb8iota.1	⊢ Ⅎ𝑦𝜑

Assertion

Ref	Expression
sb8iota	⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑)

Proof of Theorem sb8iota

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

Step	Hyp	Ref	Expression
1		nfv 1830	. . . . . 6 ⊢ Ⅎ𝑤(𝜑 ↔ 𝑥 = 𝑧)
2	1	sb8 2412	. . . . 5 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) ↔ ∀𝑤[𝑤 / 𝑥](𝜑 ↔ 𝑥 = 𝑧))
3		sbbi 2389	. . . . . . 7 ⊢ ([𝑤 / 𝑥](𝜑 ↔ 𝑥 = 𝑧) ↔ ([𝑤 / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝑥 = 𝑧))
4		sb8iota.1	. . . . . . . . 9 ⊢ Ⅎ𝑦𝜑
5	4	nfsb 2428	. . . . . . . 8 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝜑
6		equsb3 2420	. . . . . . . . 9 ⊢ ([𝑤 / 𝑥]𝑥 = 𝑧 ↔ 𝑤 = 𝑧)
7		nfv 1830	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑤 = 𝑧
8	6, 7	nfxfr 1771	. . . . . . . 8 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑥 = 𝑧
9	5, 8	nfbi 1821	. . . . . . 7 ⊢ Ⅎ𝑦([𝑤 / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝑥 = 𝑧)
10	3, 9	nfxfr 1771	. . . . . 6 ⊢ Ⅎ𝑦[𝑤 / 𝑥](𝜑 ↔ 𝑥 = 𝑧)
11		nfv 1830	. . . . . 6 ⊢ Ⅎ𝑤[𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑧)
12		sbequ 2364	. . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥](𝜑 ↔ 𝑥 = 𝑧) ↔ [𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑧)))
13	10, 11, 12	cbval 2259	. . . . 5 ⊢ (∀𝑤[𝑤 / 𝑥](𝜑 ↔ 𝑥 = 𝑧) ↔ ∀𝑦[𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑧))
14		equsb3 2420	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑧 ↔ 𝑦 = 𝑧)
15	14	sblbis 2392	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑧) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧))
16	15	albii 1737	. . . . 5 ⊢ (∀𝑦[𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑧) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧))
17	2, 13, 16	3bitri 285	. . . 4 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧))
18	17	abbii 2726	. . 3 ⊢ {𝑧 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)} = {𝑧 ∣ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧)}
19	18	unieqi 4381	. 2 ⊢ ∪ {𝑧 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)} = ∪ {𝑧 ∣ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧)}
20		dfiota2 5769	. 2 ⊢ (℩𝑥𝜑) = ∪ {𝑧 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)}
21		dfiota2 5769	. 2 ⊢ (℩𝑦[𝑦 / 𝑥]𝜑) = ∪ {𝑧 ∣ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧)}
22	19, 20, 21	3eqtr4i 2642	1 ⊢ (℩𝑥𝜑) = (℩𝑦[𝑦 / 𝑥]𝜑)

Syntax hints:   ↔ wb 195  ∀wal 1473   = wceq 1475  Ⅎwnf 1699  [wsb 1867  {cab 2596  ∪ cuni 4372  ℩cio 5766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-sn 4126  df-uni 4373  df-iota 5768

This theorem is referenced by: (None)