Description: If two formulas are equivalent for all x , then nonfreeness of x in one of them is equivalent to nonfreeness in the other. Compare nfbiit . From this and bj-nnfim and bj-nnfnt , one can prove analogous nonfreeness conservation results for other propositional operators. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht ) in order not to require sp (modal T). (Contributed by BJ, 27-Aug-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-nnfbi | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( Ⅎ' 𝑥 𝜑 ↔ Ⅎ' 𝑥 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-hbyfrbi | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑥 𝜑 → 𝜑 ) ↔ ( ∃ 𝑥 𝜓 → 𝜓 ) ) ) | |
| 2 | bj-hbxfrbi | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( 𝜓 → ∀ 𝑥 𝜓 ) ) ) | |
| 3 | 1 2 | anbi12d | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ↔ ( ( ∃ 𝑥 𝜓 → 𝜓 ) ∧ ( 𝜓 → ∀ 𝑥 𝜓 ) ) ) ) |
| 4 | df-bj-nnf | ⊢ ( Ⅎ' 𝑥 𝜑 ↔ ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) | |
| 5 | df-bj-nnf | ⊢ ( Ⅎ' 𝑥 𝜓 ↔ ( ( ∃ 𝑥 𝜓 → 𝜓 ) ∧ ( 𝜓 → ∀ 𝑥 𝜓 ) ) ) | |
| 6 | 3 4 5 | 3bitr4g | ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) → ( Ⅎ' 𝑥 𝜑 ↔ Ⅎ' 𝑥 𝜓 ) ) |