Theorem iotajust 6453

Description: Soundness justification theorem for df-iota 6454. (Contributed by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
iotajust	⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}

Distinct variable groups:   𝑥,𝑧   𝜑,𝑧   𝜑,𝑦   𝑥,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem iotajust

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sneq 4577	. . . . 5 ⊢ (𝑦 = 𝑤 → {𝑦} = {𝑤})
2	1	eqeq2d 2747	. . . 4 ⊢ (𝑦 = 𝑤 → ({𝑥 ∣ 𝜑} = {𝑦} ↔ {𝑥 ∣ 𝜑} = {𝑤}))
3	2	cbvabv 2806	. . 3 ⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}}
4		sneq 4577	. . . . 5 ⊢ (𝑤 = 𝑧 → {𝑤} = {𝑧})
5	4	eqeq2d 2747	. . . 4 ⊢ (𝑤 = 𝑧 → ({𝑥 ∣ 𝜑} = {𝑤} ↔ {𝑥 ∣ 𝜑} = {𝑧}))
6	5	cbvabv 2806	. . 3 ⊢ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} = {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
7	3, 6	eqtri 2759	. 2 ⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
8	7	unieqi 4862	1 ⊢ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}

Syntax hints:   = wceq 1542  {cab 2714  {csn 4567  ∪ cuni 4850

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-sn 4568  df-uni 4851

This theorem is referenced by: (None)