![]() |
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 cbvrexfw 3300 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvralw.1 | ⊢ Ⅎ𝑦𝜑 |
cbvralw.2 | ⊢ Ⅎ𝑥𝜓 |
cbvralw.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrexw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2901 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2901 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvralw.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvralw.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvralw.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvrexfw 3300 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 Ⅎwnf 1783 ∃wrex 3068 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-11 2152 ax-12 2169 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-ex 1780 df-nf 1784 df-clel 2808 df-nfc 2883 df-ral 3060 df-rex 3069 |
This theorem is referenced by: cbvrexsvw 3313 cbvrexsvwOLD 3315 cbvreuw 3404 cbvrmowOLD 3409 reu8nf 3870 cbviun 5038 isarep1 6636 isarep1OLD 6637 fvelimad 6958 dffo3f 7106 elabrex 7243 elabrexg 7244 onminex 7792 boxcutc 8937 indexfi 9362 wdom2d 9577 hsmexlem2 10424 fprodle 15944 iundisj 25297 mbfsup 25413 iundisjf 32087 iundisjfi 32274 voliune 33525 volfiniune 33526 bnj1542 34166 cvmcov 34552 poimirlem24 36815 poimirlem26 36817 indexa 36904 rexrabdioph 41834 rexfrabdioph 41835 disjrnmpt2 44185 caucvgbf 44498 limsuppnfd 44716 limsuppnf 44725 limsupre2 44739 limsupre3 44747 limsupre3uz 44750 limsupreuz 44751 liminfreuz 44817 stoweidlem31 45045 stoweidlem59 45073 rexsb 46105 cbvrex2 46110 2reu8i 46119 |
Copyright terms: Public domain | W3C validator |