Nearby theorems
|
|
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-rnf | Structured version Visualization version Unicode version | ||
Description: Definition of restricted
non-freeness. Informally, the proposition
     means
that   does not vary on .
(Contributed by BJ, 19-Mar-2021.) |
| Ref | Expression |
|---|---|
| df-bj-rnf |
     |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . 3
 | |
| 2 | vx |
. . 3
 | |
| 3 | cA |
. . 3
 | |
| 4 | 1, 2, 3 | wrnf 32930 |
. 2
|
| 5 | 1, 2, 3 | wrex 2913 |
. . 3
|
| 6 | 1, 2, 3 | wral 2912 |
. . 3
|
| 7 | 5, 6 | wi 4 |
. 2
|
| 8 | 4, 7 | wb 196 |
1
|
| Colors of variables: wff setvar class |
| This definition is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |