Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvrexw | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. Version of cbvrex 3446 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvralw.1 | ⊢ Ⅎ𝑦𝜑 |
cbvralw.2 | ⊢ Ⅎ𝑥𝜓 |
cbvralw.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrexw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2977 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2977 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvralw.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvralw.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvralw.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvrexfw 3438 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 Ⅎwnf 1784 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-10 2145 ax-11 2161 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-nf 1785 df-sb 2070 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 |
This theorem is referenced by: cbvrmow 3444 cbvrexsvw 3468 reu8nf 3860 cbviun 4961 isarep1 6442 fvelimad 6732 elabrex 7002 onminex 7522 boxcutc 8505 indexfi 8832 wdom2d 9044 hsmexlem2 9849 fprodle 15350 iundisj 24149 mbfsup 24265 iundisjf 30339 iundisjfi 30519 voliune 31488 volfiniune 31489 bnj1542 32129 cvmcov 32510 poimirlem24 34931 poimirlem26 34933 indexa 35023 rexrabdioph 39440 rexfrabdioph 39441 elabrexg 41352 dffo3f 41487 disjrnmpt2 41498 limsuppnfd 42032 limsuppnf 42041 limsupre2 42055 limsupre3 42063 limsupre3uz 42066 limsupreuz 42067 liminfreuz 42133 stoweidlem31 42365 stoweidlem59 42393 rexsb 43346 2reu8i 43361 |
Copyright terms: Public domain | W3C validator |