![]() |
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 3287 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2371. (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvralw.1 | ⊢ Ⅎ𝑦𝜑 |
cbvralw.2 | ⊢ Ⅎ𝑥𝜓 |
cbvralw.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrexw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2904 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2904 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvralw.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvralw.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvralw.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvrexfw 3287 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 Ⅎwnf 1786 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-nf 1787 df-clel 2811 df-nfc 2886 df-ral 3062 df-rex 3071 |
This theorem is referenced by: cbvrexsvw 3300 cbvreuw 3382 cbvrmowOLD 3387 reu8nf 3834 cbviun 4997 isarep1 6591 isarep1OLD 6592 fvelimad 6910 elabrex 7191 onminex 7738 boxcutc 8882 indexfi 9307 wdom2d 9521 hsmexlem2 10368 fprodle 15884 iundisj 24928 mbfsup 25044 iundisjf 31553 iundisjfi 31746 voliune 32885 volfiniune 32886 bnj1542 33526 cvmcov 33914 poimirlem24 36148 poimirlem26 36150 indexa 36238 rexrabdioph 41160 rexfrabdioph 41161 elabrexg 43337 dffo3f 43486 disjrnmpt2 43495 caucvgbf 43811 limsuppnfd 44029 limsuppnf 44038 limsupre2 44052 limsupre3 44060 limsupre3uz 44063 limsupreuz 44064 liminfreuz 44130 stoweidlem31 44358 stoweidlem59 44386 rexsb 45417 cbvrex2 45422 2reu8i 45431 |
Copyright terms: Public domain | W3C validator |