![]() |
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. (Contributed by NM, 26-May-1999.) |
Ref | Expression |
---|---|
cbvabv.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvabv | ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1984 | . 2 ⊢ Ⅎ𝑦𝜑 | |
2 | nfv 1984 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | cbvabv.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | cbvab 2876 | 1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1624 {cab 2738 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 |
This theorem is referenced by: cdeqab1 3560 difjust 3709 unjust 3711 injust 3713 uniiunlem 3825 dfif3 4236 pwjust 4295 snjust 4312 intab 4651 intabs 4966 iotajust 6003 wfrlem1 7575 sbth 8237 cardprc 8988 iunfictbso 9119 aceq3lem 9125 isf33lem 9372 axdc3 9460 axdclem 9525 axdc 9527 genpv 10005 ltexpri 10049 recexpr 10057 supsr 10117 hashf1lem2 13424 cvbtrcl 13924 mertens 14809 4sq 15862 isuhgr 26146 isushgr 26147 isupgr 26170 isumgr 26181 isuspgr 26238 isusgr 26239 isconngr 27333 isconngr1 27334 isfrgr 27404 dispcmp 30227 eulerpart 30745 ballotlemfmpn 30857 bnj66 31229 bnj1234 31380 subfacp1lem6 31466 subfacp1 31467 dfon2lem3 31987 dfon2lem7 31991 frrlem1 32078 nosupdm 32148 f1omptsn 33487 ismblfin 33755 glbconxN 35159 eldioph3 37823 diophrex 37833 cbvcllem 38409 ssfiunibd 40014 |
Copyright terms: Public domain | W3C validator |