![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvriotavw | Structured version Visualization version GIF version |
Description: Change bound variable in a restricted description binder. Version of cbvriotav 7402 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.) |
Ref | Expression |
---|---|
cbvriotavw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvriotavw | ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1w 2822 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
2 | cbvriotavw.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | anbi12d 632 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
4 | 3 | cbviotavw 6524 | . 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) |
5 | df-riota 7388 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
6 | df-riota 7388 | . 2 ⊢ (℩𝑦 ∈ 𝐴 𝜓) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) | |
7 | 4, 5, 6 | 3eqtr4i 2773 | 1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ℩cio 6514 ℩crio 7387 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-ss 3980 df-uni 4913 df-iota 6516 df-riota 7388 |
This theorem is referenced by: ordtypecbv 9555 fin23lem27 10366 zorn2g 10541 nosupcbv 27762 noinfcbv 27777 uspgredg2v 29256 usgredg2v 29259 cnlnadji 32105 nmopadjlei 32117 cvmliftlem15 35283 cvmliftiota 35286 cvmlift2 35301 cvmlift3lem7 35310 cvmlift3 35313 weiunlem2 36446 lshpkrlem3 39094 cdleme40v 40452 lcfl7N 41484 lcf1o 41534 lcfrlem39 41564 hdmap1cbv 41785 wessf1ornlem 45128 fourierdlem103 46165 fourierdlem104 46166 |
Copyright terms: Public domain | W3C validator |