![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvrex | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Ref | Expression |
---|---|
cbvral.1 | ⊢ Ⅎ𝑦𝜑 |
cbvral.2 | ⊢ Ⅎ𝑥𝜓 |
cbvral.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrex | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2925 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2925 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvral.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvral.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvral.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvrexf 3371 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 Ⅎwnf 1747 ∃wrex 3082 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clel 2839 df-nfc 2911 df-ral 3086 df-rex 3087 |
This theorem is referenced by: cbvrmo 3375 cbvrexv 3377 cbvrexsv 3389 reu8nf 3756 cbviun 4827 isarep1 6272 fvelimad 6559 elabrex 6825 onminex 7336 boxcutc 8300 indexfi 8625 wdom2d 8837 hsmexlem2 9645 fprodle 15208 iundisj 23867 mbfsup 23983 iundisjf 30122 iundisjfi 30292 voliune 31165 volfiniune 31166 bnj1542 31808 cvmcov 32132 poimirlem24 34394 poimirlem26 34396 indexa 34487 rexrabdioph 38825 rexfrabdioph 38826 elabrexg 40760 dffo3f 40897 disjrnmpt2 40908 limsuppnfd 41448 climinf2 41453 limsuppnf 41457 limsupre2 41471 limsupre3 41479 limsupre3uz 41482 limsupreuz 41483 liminfreuz 41549 stoweidlem31 41781 stoweidlem59 41809 meaiunincf 42230 rexsb 42737 cbvrex2 42742 2reu8i 42752 |
Copyright terms: Public domain | W3C validator |