![]() |
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 7382 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, 30-Sep-2024.) |
Ref | Expression |
---|---|
cbvriotavw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvriotavw | ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1w 2814 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
2 | cbvriotavw.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | anbi12d 629 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
4 | 3 | cbviotavw 6502 | . 2 ⊢ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) |
5 | df-riota 7367 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
6 | df-riota 7367 | . 2 ⊢ (℩𝑦 ∈ 𝐴 𝜓) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) | |
7 | 4, 5, 6 | 3eqtr4i 2768 | 1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1539 ∈ wcel 2104 ℩cio 6492 ℩crio 7366 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-in 3954 df-ss 3964 df-uni 4908 df-iota 6494 df-riota 7367 |
This theorem is referenced by: ordtypecbv 9514 fin23lem27 10325 zorn2g 10500 nosupcbv 27441 noinfcbv 27456 uspgredg2v 28748 usgredg2v 28751 cnlnadji 31596 nmopadjlei 31608 cvmliftlem15 34587 cvmliftiota 34590 cvmlift2 34605 cvmlift3lem7 34614 cvmlift3 34617 lshpkrlem3 38285 cdleme40v 39643 lcfl7N 40675 lcf1o 40725 lcfrlem39 40755 hdmap1cbv 40976 wessf1ornlem 44182 fourierdlem103 45223 fourierdlem104 45224 |
Copyright terms: Public domain | W3C validator |