![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvriotav | Structured version Visualization version GIF version |
Description: Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
cbvriotav.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvriotav | ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1957 | . 2 ⊢ Ⅎ𝑦𝜑 | |
2 | nfv 1957 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | cbvriotav.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | cbvriota 6893 | 1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 ℩crio 6882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-rex 3096 df-sn 4399 df-uni 4672 df-iota 6099 df-riota 6883 |
This theorem is referenced by: ordtypecbv 8711 fin23lem27 9485 zorn2g 9660 uspgredg2v 26570 usgredg2v 26573 cnlnadji 29507 nmopadjlei 29519 cvmliftlem15 31879 cvmliftiota 31882 cvmlift2 31897 cvmlift3lem7 31906 cvmlift3 31909 lshpkrlem3 35268 cdleme40v 36625 lcfl7N 37657 lcf1o 37707 lcfrlem39 37737 hdmap1cbv 37958 wessf1ornlem 40298 fourierdlem103 41357 fourierdlem104 41358 |
Copyright terms: Public domain | W3C validator |