Theorem cbviotavw 6533

Description: Change bound variables in a description binder. Version of cbviotav 6536 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 2815	. . . . 5 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
3	2	eqeq1i 2745	. . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑧} ↔ {𝑦 ∣ 𝜓} = {𝑧})
4	3	abbii 2812	. . 3 ⊢ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
5	4	unieqi 4943	. 2 ⊢ ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
6		df-iota 6525	. 2 ⊢ (℩𝑥𝜑) = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
7		df-iota 6525	. 2 ⊢ (℩𝑦𝜓) = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}}
8	5, 6, 7	3eqtr4i 2778	1 ⊢ (℩𝑥𝜑) = (℩𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  {cab 2717  {csn 4648  ∪ cuni 4931  ℩cio 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-iota 6525

This theorem is referenced by:  cbvriotavw  7414  oeeui  8658  nosupcbv  27765  noinfcbv  27780  cbvriotavw2  36202  ellimciota  45535  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem105  46132  fourierdlem106  46133  fourierdlem108  46135  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  fourierdlem115  46142  funressndmafv2rn  47138