Description: Deduction form of dvelimf . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 7-Apr-2004) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvelimdf.1 | |- F/ x ph |
|
dvelimdf.2 | |- F/ z ph |
||
dvelimdf.3 | |- ( ph -> F/ x ps ) |
||
dvelimdf.4 | |- ( ph -> F/ z ch ) |
||
dvelimdf.5 | |- ( ph -> ( z = y -> ( ps <-> ch ) ) ) |
||
Assertion | dvelimdf | |- ( ph -> ( -. A. x x = y -> F/ x ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvelimdf.1 | |- F/ x ph |
|
2 | dvelimdf.2 | |- F/ z ph |
|
3 | dvelimdf.3 | |- ( ph -> F/ x ps ) |
|
4 | dvelimdf.4 | |- ( ph -> F/ z ch ) |
|
5 | dvelimdf.5 | |- ( ph -> ( z = y -> ( ps <-> ch ) ) ) |
|
6 | 1 3 | nfim1 | |- F/ x ( ph -> ps ) |
7 | 2 4 | nfim1 | |- F/ z ( ph -> ch ) |
8 | 5 | com12 | |- ( z = y -> ( ph -> ( ps <-> ch ) ) ) |
9 | 8 | pm5.74d | |- ( z = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) ) |
10 | 6 7 9 | dvelimf | |- ( -. A. x x = y -> F/ x ( ph -> ch ) ) |
11 | pm5.5 | |- ( ph -> ( ( ph -> ch ) <-> ch ) ) |
|
12 | 1 11 | nfbidf | |- ( ph -> ( F/ x ( ph -> ch ) <-> F/ x ch ) ) |
13 | 10 12 | syl5ib | |- ( ph -> ( -. A. x x = y -> F/ x ch ) ) |