| 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 2814 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2157 and ax-13 2377. (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 2100 | . . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓) |
| 3 | df-clab 2715 | . . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑) | |
| 4 | df-clab 2715 | . . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | . 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓}) |
| 6 | 5 | eqriv 2734 | 1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 [wsb 2064 ∈ wcel 2108 {cab 2714 |
| 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 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 |
| This theorem is referenced by: cbvrabv 3447 cbvsbcvw 3822 difjust 3953 unjust 3955 injust 3957 uniiunlem 4087 dfif3 4540 pwjust 4601 snjust 4625 intab 4978 intabs 5349 iotajust 6513 cbviotavw 6522 frrlem1 8311 wfrlem1OLD 8348 fsetprcnex 8902 sbth 9133 sbthfi 9239 cardprc 10020 iunfictbso 10154 aceq3lem 10160 isf33lem 10406 axdc3 10494 axdclem 10559 axdc 10561 genpv 11039 ltexpri 11083 recexpr 11091 supsr 11152 hashf1lem2 14495 cvbtrcl 15031 mertens 15922 4sq 17002 symgval 19388 nosupcbv 27747 nosupdm 27749 noinfcbv 27762 noinfdm 27764 addsval2 27996 addscut 28011 addsunif 28035 addsasslem1 28036 addsasslem2 28037 mulsval2lem 28136 mulsunif2 28196 precsexlemcbv 28230 isuhgr 29077 isushgr 29078 isupgr 29101 isumgr 29112 isuspgr 29169 isusgr 29170 isconngr 30208 isconngr1 30209 dispcmp 33858 eulerpart 34384 ballotlemfmpn 34497 bnj66 34874 bnj1234 35027 subfacp1lem6 35190 subfacp1 35191 dfon2lem3 35786 dfon2lem7 35790 cbvsbcvw2 36231 cbvixpvw2 36246 bj-gabeqis 36939 f1omptsn 37338 rdgssun 37379 ismblfin 37668 glbconxN 39380 sticksstones15 42162 eldioph3 42777 diophrex 42786 cbvcllem 43622 cbvrabv2w 45133 ssfiunibd 45321 aiotajust 47096 |
| Copyright terms: Public domain | W3C validator |