![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbval | Structured version Visualization version Unicode version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Ref | Expression |
---|---|
cbval.1 |
![]() ![]() ![]() ![]() |
cbval.2 |
![]() ![]() ![]() ![]() |
cbval.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cbval |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbval.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | cbval.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | cbval.3 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | biimpd 212 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 4 | cbv3 2108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3 | biimprd 231 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | equcoms 1867 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 2, 1, 7 | cbv3 2108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 5, 8 | impbii 192 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1667 df-nf 1671 |
This theorem is referenced by: cbvex 2115 cbvalv 2116 cbval2 2120 sb8 2253 sb8eu 2332 cbvralf 2980 ralab2 3170 cbvralcsf 3362 dfss2f 3390 elintab 4214 reusv2lem4 4579 cbviota 5529 sb8iota 5531 dffun6f 5574 findcard2 7797 aceq1 8534 bnj1385 29649 bnj1476 29663 sbcalf 32353 alrimii 32360 aomclem6 35918 rababg 36180 dfcleqf 37426 stoweidlem34 37951 |
Copyright terms: Public domain | W3C validator |