![]() |
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 2913 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2913 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvral.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvral.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvral.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvrexf 3315 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 Ⅎwnf 1856 ∃wrex 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 |
This theorem is referenced by: cbvrmo 3319 cbvrexv 3321 cbvrexsv 3332 reu8nf 3665 cbviun 4691 isarep1 6117 elabrex 6644 onminex 7154 boxcutc 8105 indexfi 8430 wdom2d 8641 hsmexlem2 9451 fprodle 14933 iundisj 23536 mbfsup 23651 iundisjf 29740 iundisjfi 29895 voliune 30632 volfiniune 30633 bnj1542 31265 cvmcov 31583 poimirlem24 33766 poimirlem26 33768 indexa 33860 rexrabdioph 37884 rexfrabdioph 37885 elabrexg 39728 dffo3f 39884 disjrnmpt2 39895 fvelimad 39976 limsuppnfd 40452 climinf2 40457 limsuppnf 40461 limsupre2 40475 limsupre3 40483 limsupre3uz 40486 limsupreuz 40487 liminfreuz 40553 stoweidlem31 40765 stoweidlem59 40793 meaiunincf 41217 rexsb 41688 cbvrex2 41693 |
Copyright terms: Public domain | W3C validator |