Theorem cbviotavw 6449

Description: Change bound variables in a description binder. Version of cbviotav 6451 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 2809	. . . . 5 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
3	2	eqeq1i 2744	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑧} ↔ {𝑦 ∣ 𝜓} = {𝑧})
4	3	abbii 2806	. . 3 ⊢ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
5	4	unieqi 4850	. 2 ⊢ ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
6		df-iota 6441	. 2 ⊢ (℩𝑥𝜑) = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
7		df-iota 6441	. 2 ⊢ (℩𝑦𝜓) = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
8	5, 6, 7	3eqtr4i 2772	1 ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  {cab 2717  {csn 4555  ∪ cuni 4838  ℩cio 6439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-uni 4839  df-iota 6441

This theorem is referenced by:  cbvriotavw  7323  oeeui  8528  nosupcbv  27684  noinfcbv  27699  cbvriotavw2  36464  ellimciota  46059  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem105  46654  fourierdlem106  46655  fourierdlem108  46657  fourierdlem110  46659  fourierdlem112  46661  fourierdlem113  46662  fourierdlem115  46664  funressndmafv2rn  47686