Description: An equality theorem for nonfreeness. See nfbidf for a version without disjoint variable condition but requiring more axioms. (Contributed by Mario Carneiro, 4-Oct-2016) Remove dependency on ax-6 , ax-7 , ax-12 by adapting proof of nfbidf . (Revised by BJ, 25-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | albidv.1 | |- ( ph -> ( ps <-> ch ) ) |
|
| Assertion | nfbidv | |- ( ph -> ( F/ x ps <-> F/ x ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | albidv.1 | |- ( ph -> ( ps <-> ch ) ) |
|
| 2 | 1 | exbidv | |- ( ph -> ( E. x ps <-> E. x ch ) ) |
| 3 | 1 | albidv | |- ( ph -> ( A. x ps <-> A. x ch ) ) |
| 4 | 2 3 | imbi12d | |- ( ph -> ( ( E. x ps -> A. x ps ) <-> ( E. x ch -> A. x ch ) ) ) |
| 5 | df-nf | |- ( F/ x ps <-> ( E. x ps -> A. x ps ) ) |
|
| 6 | df-nf | |- ( F/ x ch <-> ( E. x ch -> A. x ch ) ) |
|
| 7 | 4 5 6 | 3bitr4g | |- ( ph -> ( F/ x ps <-> F/ x ch ) ) |