| 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 3305 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.) |
| Ref | Expression |
|---|---|
| cbvralw.1 | ⊢ Ⅎ𝑦𝜑 |
| cbvralw.2 | ⊢ Ⅎ𝑥𝜓 |
| cbvralw.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| cbvrexw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfcv 2905 | . 2 ⊢ Ⅎ𝑥𝐴 | |
| 2 | nfcv 2905 | . 2 ⊢ Ⅎ𝑦𝐴 | |
| 3 | cbvralw.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
| 4 | cbvralw.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
| 5 | cbvralw.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 6 | 1, 2, 3, 4, 5 | cbvrexfw 3305 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 Ⅎwnf 1783 ∃wrex 3070 |
| 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-8 2110 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: cbvrexsvw 3318 cbvrexsvwOLD 3321 cbvreuw 3410 reu8nf 3877 cbviun 5036 isarep1 6656 isarep1OLD 6657 fvelimad 6976 dffo3f 7126 elabrex 7262 elabrexg 7263 onminex 7822 boxcutc 8981 indexfi 9400 wdom2d 9620 hsmexlem2 10467 fprodle 16032 iundisj 25583 mbfsup 25699 iundisjf 32602 iundisjfi 32798 voliune 34230 volfiniune 34231 bnj1542 34871 cvmcov 35268 poimirlem24 37651 poimirlem26 37653 indexa 37740 mndmolinv 42096 primrootsunit1 42098 primrootsunit 42099 primrootspoweq0 42107 aks6d1c4 42125 aks6d1c6isolem1 42175 aks6d1c6isolem2 42176 rhmqusspan 42186 grpods 42195 unitscyglem1 42196 unitscyglem3 42198 unitscyglem4 42199 rexrabdioph 42805 rexfrabdioph 42806 disjrnmpt2 45193 caucvgbf 45500 limsuppnfd 45717 limsuppnf 45726 limsupre2 45740 limsupre3 45748 limsupre3uz 45751 limsupreuz 45752 liminfreuz 45818 stoweidlem31 46046 stoweidlem59 46074 rexsb 47111 cbvrex2 47116 2reu8i 47125 |
| Copyright terms: Public domain | W3C validator |