Theorem cbviotavw 6460

Description: Change bound variables in a description binder. Version of cbviotav 6462 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.)

Hypothesis

Ref	Expression
cbviotavw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbviotavw	⊢ (℩𝑥𝜑) = (℩𝑦𝜓)

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

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

Proof of Theorem cbviotavw

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cbviotavw.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	cbvabv 2799	. . . . 5 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
3	2	eqeq1i 2734	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑧} ↔ {𝑦 ∣ 𝜓} = {𝑧})
4	3	abbii 2796	. . 3 ⊢ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
5	4	unieqi 4879	. 2 ⊢ ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
6		df-iota 6452	. 2 ⊢ (℩𝑥𝜑) = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
7		df-iota 6452	. 2 ⊢ (℩𝑦𝜓) = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
8	5, 6, 7	3eqtr4i 2762	1 ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  {cab 2707  {csn 4585  ∪ cuni 4867  ℩cio 6450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868  df-iota 6452

This theorem is referenced by:  cbvriotavw  7336  oeeui  8543  nosupcbv  27590  noinfcbv  27605  cbvriotavw2  36197  ellimciota  45585  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem105  46182  fourierdlem106  46183  fourierdlem108  46185  fourierdlem110  46187  fourierdlem112  46189  fourierdlem113  46190  fourierdlem115  46192  funressndmafv2rn  47197