![]() |
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 6507 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 2806 | . . . . 5 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
3 | 2 | eqeq1i 2738 | . . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑧} ↔ {𝑦 ∣ 𝜓} = {𝑧}) |
4 | 3 | abbii 2803 | . . 3 ⊢ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}} |
5 | 4 | unieqi 4922 | . 2 ⊢ ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}} |
6 | df-iota 6496 | . 2 ⊢ (℩𝑥𝜑) = ∪ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | |
7 | df-iota 6496 | . 2 ⊢ (℩𝑦𝜓) = ∪ {𝑧 ∣ {𝑦 ∣ 𝜓} = {𝑧}} | |
8 | 5, 6, 7 | 3eqtr4i 2771 | 1 ⊢ (℩𝑥𝜑) = (℩𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 {cab 2710 {csn 4629 ∪ cuni 4909 ℩cio 6494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-uni 4910 df-iota 6496 |
This theorem is referenced by: cbvriotavw 7375 oeeui 8602 nosupcbv 27205 noinfcbv 27220 ellimciota 44330 fourierdlem96 44918 fourierdlem97 44919 fourierdlem98 44920 fourierdlem99 44921 fourierdlem105 44927 fourierdlem106 44928 fourierdlem108 44930 fourierdlem110 44932 fourierdlem112 44934 fourierdlem113 44935 fourierdlem115 44937 funressndmafv2rn 45931 |
Copyright terms: Public domain | W3C validator |