Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-dvelimdv | Structured version Visualization version Unicode version |
Description: Deduction form of dvelim 2337 with DV conditions. Uncurried (imported)
form of bj-dvelimdv 32834. Typically, is a fresh variable used for
the implicit substitution hypothesis that results in (namely,
can be
thought as and as
). So the theorem says that
if x is effectively free
in , then if x and y are not the
same variable, then
is also
effectively free in , in a context
.
One can weakend the implicit substitution hypothesis by adding the antecedent but this typically does not make the theorem much more useful. Similarly, one could use non-freeness hypotheses instead of DV conditions but since this result is typically used when is a dummy variable, this would not be of much benefit. One could also remove DV(z,x) since in the proof nfv 1843 can be replaced with nfal 2153 followed by nfn 1784. Remark: nfald 2165 uses ax-11 2034; it might be possible to inline and use ax11w 2007 instead, but there is still a use via 19.12 2164 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-dvelimdv.nf | |
bj-dvelimdv.nf1 | |
bj-dvelimdv.is |
Ref | Expression |
---|---|
bj-dvelimdv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-dvelimdv.is | . . . 4 | |
2 | 1 | equsalvw 1931 | . . 3 |
3 | 2 | bicomi 214 | . 2 |
4 | nfv 1843 | . . . 4 | |
5 | nfv 1843 | . . . 4 | |
6 | 4, 5 | nfan 1828 | . . 3 |
7 | nfeqf2 2297 | . . . . 5 | |
8 | 7 | adantl 482 | . . . 4 |
9 | bj-dvelimdv.nf1 | . . . . 5 | |
10 | 9 | adantr 481 | . . . 4 |
11 | 8, 10 | nfimd 1823 | . . 3 |
12 | 6, 11 | nfald 2165 | . 2 |
13 | 3, 12 | nfxfrd 1780 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wa 384 wal 1481 wnf 1708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |