Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbviotavw | Structured version Visualization version GIF version |
Description: Change bound variables in a description binder. Version of cbviotav 6349 with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by Gino Giotto, 30-Sep-2024.) |
Ref | Expression |
---|---|
cbviotavw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbviotavw | ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbviotavw.1 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
2 | 1 | cbvabv 2811 | . . . . 5 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
3 | 2 | eqeq1i 2742 | . . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑧} ↔ {𝑦 ∣ 𝜓} = {𝑧}) |
4 | 3 | abbii 2808 | . . 3 ⊢ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}} |
5 | 4 | unieqi 4832 | . 2 ⊢ ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}} |
6 | df-iota 6338 | . 2 ⊢ (℩𝑥𝜑) = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | |
7 | df-iota 6338 | . 2 ⊢ (℩𝑦𝜓) = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}} | |
8 | 5, 6, 7 | 3eqtr4i 2775 | 1 ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1543 {cab 2714 {csn 4541 ∪ cuni 4819 ℩cio 6336 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 df-uni 4820 df-iota 6338 |
This theorem is referenced by: cbvriotavw 7180 oeeui 8330 nosupcbv 33642 noinfcbv 33657 ellimciota 42830 fourierdlem96 43418 fourierdlem97 43419 fourierdlem98 43420 fourierdlem99 43421 fourierdlem105 43427 fourierdlem106 43428 fourierdlem108 43430 fourierdlem110 43432 fourierdlem112 43434 fourierdlem113 43435 fourierdlem115 43437 funressndmafv2rn 44387 |
Copyright terms: Public domain | W3C validator |