![]() |
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 2801 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2147 and ax-13 2366. (Revised by Steven Nguyen, 4-Dec-2022.) |
Ref | Expression |
---|---|
cbvabv.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvabv | ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvabv.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
2 | 1 | cbvsbv 2354 | . . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓) |
3 | df-clab 2704 | . . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑) | |
4 | df-clab 2704 | . . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓) | |
5 | 2, 3, 4 | 3bitr4i 302 | . 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓}) |
6 | 5 | eqriv 2723 | 1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 [wsb 2060 ∈ wcel 2099 {cab 2703 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 |
This theorem is referenced by: cbvrabv 3430 cbvsbcvw 3811 difjust 3949 unjust 3951 injust 3953 uniiunlem 4083 dfif3 4547 pwjust 4608 snjust 4632 intab 4986 intabs 5349 iotajust 6505 cbviotavw 6514 frrlem1 8301 wfrlem1OLD 8338 fsetprcnex 8891 sbth 9131 sbthfi 9236 cardprc 10023 iunfictbso 10157 aceq3lem 10163 isf33lem 10409 axdc3 10497 axdclem 10562 axdc 10564 genpv 11042 ltexpri 11086 recexpr 11094 supsr 11155 hashf1lem2 14475 cvbtrcl 14997 mertens 15890 4sq 16966 symgval 19366 nosupcbv 27732 nosupdm 27734 noinfcbv 27747 noinfdm 27749 addsval2 27977 addscut 27992 addsunif 28016 addsasslem1 28017 addsasslem2 28018 mulsval2lem 28111 mulsunif2 28171 precsexlemcbv 28205 isuhgr 28996 isushgr 28997 isupgr 29020 isumgr 29031 isuspgr 29088 isusgr 29089 isconngr 30122 isconngr1 30123 dispcmp 33674 eulerpart 34216 ballotlemfmpn 34328 bnj66 34705 bnj1234 34858 subfacp1lem6 35013 subfacp1 35014 dfon2lem3 35609 dfon2lem7 35613 bj-gabeqis 36644 f1omptsn 37044 rdgssun 37085 ismblfin 37362 glbconxN 39077 sticksstones15 41859 eldioph3 42423 diophrex 42432 cbvcllem 43276 ssfiunibd 44924 aiotajust 46697 |
Copyright terms: Public domain | W3C validator |