![]() |
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 3303 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2375. (Revised by GG, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvralw.1 | ⊢ Ⅎ𝑦𝜑 |
cbvralw.2 | ⊢ Ⅎ𝑥𝜓 |
cbvralw.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrexw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2903 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2903 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvralw.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvralw.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvralw.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvrexfw 3303 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 Ⅎwnf 1780 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-11 2155 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 df-clel 2814 df-nfc 2890 df-ral 3060 df-rex 3069 |
This theorem is referenced by: cbvrexsvw 3316 cbvrexsvwOLD 3319 cbvreuw 3408 reu8nf 3886 cbviun 5041 isarep1 6657 isarep1OLD 6658 fvelimad 6976 dffo3f 7126 elabrex 7262 elabrexg 7263 onminex 7822 boxcutc 8980 indexfi 9398 wdom2d 9618 hsmexlem2 10465 fprodle 16029 iundisj 25597 mbfsup 25713 iundisjf 32609 iundisjfi 32804 voliune 34210 volfiniune 34211 bnj1542 34850 cvmcov 35248 poimirlem24 37631 poimirlem26 37633 indexa 37720 mndmolinv 42077 primrootsunit1 42079 primrootsunit 42080 primrootspoweq0 42088 aks6d1c4 42106 aks6d1c6isolem1 42156 aks6d1c6isolem2 42157 rhmqusspan 42167 grpods 42176 unitscyglem1 42177 unitscyglem3 42179 unitscyglem4 42180 rexrabdioph 42782 rexfrabdioph 42783 disjrnmpt2 45131 caucvgbf 45440 limsuppnfd 45658 limsuppnf 45667 limsupre2 45681 limsupre3 45689 limsupre3uz 45692 limsupreuz 45693 liminfreuz 45759 stoweidlem31 45987 stoweidlem59 46015 rexsb 47049 cbvrex2 47054 2reu8i 47063 |
Copyright terms: Public domain | W3C validator |