![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > cbvrex | Unicode 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 2619 | . 2 | |
2 | nfcv 2619 | . 2 | |
3 | cbvral.1 | . 2 | |
4 | cbvral.2 | . 2 | |
5 | cbvral.3 | . 2 | |
6 | 1, 2, 3, 4, 5 | cbvrexf 3079 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 <-> wb 184
F/ wnf 1616 E. wrex 2808 |
This theorem is referenced by: cbvrmo 3083 cbvrexv 3085 cbvrexsv 3096 cbviun 4367 isarep1 5672 elabrex 6155 onminex 6642 boxcutc 7532 indexfi 7848 wdom2d 8027 hsmexlem2 8828 iundisj 21958 mbfsup 22071 iundisjf 27448 iundisjfi 27601 voliune 28201 volfiniune 28202 cvmcov 28708 indexa 30224 rexrabdioph 30727 rexfrabdioph 30728 elabrexg 31430 fprodle 31604 stoweidlem31 31813 stoweidlem59 31841 rexsb 32173 cbvrex2 32178 bnj1542 33915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-ex 1613 df-nf 1617 df-sb 1740 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ral 2812 df-rex 2813 |
Copyright terms: Public domain | W3C validator |