![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvabv | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2906 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2094 and ax-13 2302. (Revised by Steven Nguyen, 4-Dec-2022.) |
Ref | Expression |
---|---|
cbvabv.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvabv | ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbco2vv 2045 | . . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑) | |
2 | cbvabv.1 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbievw 2042 | . . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
4 | 3 | sbbii 2028 | . . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓) |
5 | 1, 4 | bitr3i 269 | . . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓) |
6 | df-clab 2754 | . . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑) | |
7 | df-clab 2754 | . . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓) | |
8 | 5, 6, 7 | 3bitr4i 295 | . 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓}) |
9 | 8 | eqriv 2770 | 1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1508 [wsb 2016 ∈ wcel 2051 {cab 2753 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-9 2060 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 df-sb 2017 df-clab 2754 df-cleq 2766 |
This theorem is referenced by: cbvrabv 3407 difjust 3826 unjust 3828 injust 3830 uniiunlem 3946 dfif3 4359 pwjust 4418 snjust 4435 intab 4776 intabs 5098 iotajust 6149 wfrlem1 7756 sbth 8432 cardprc 9202 iunfictbso 9333 aceq3lem 9339 isf33lem 9585 axdc3 9673 axdclem 9738 axdc 9740 genpv 10218 ltexpri 10262 recexpr 10270 supsr 10331 hashf1lem2 13626 cvbtrcl 14212 mertens 15101 4sq 16155 isuhgr 26564 isushgr 26565 isupgr 26588 isumgr 26599 isuspgr 26656 isusgr 26657 isconngr 27734 isconngr1 27735 isfrgr 27808 dispcmp 30800 eulerpart 31318 ballotlemfmpn 31431 bnj66 31812 bnj1234 31963 subfacp1lem6 32050 subfacp1 32051 dfon2lem3 32583 dfon2lem7 32587 frrlem1 32677 nosupdm 32758 f1omptsn 34093 rdgssun 34134 ismblfin 34407 glbconxN 35992 eldioph3 38792 diophrex 38802 cbvcllem 39365 ssfiunibd 41035 aiotajust 42720 |
Copyright terms: Public domain | W3C validator |