This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfbidf

Description: An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021)

Ref Expression
Hypotheses albid.1 ⊢ Ⅎ x φ
albid.2 ⊢ φ → ψ ↔ χ
Assertion nfbidf ⊢ φ → Ⅎ x ψ ↔ Ⅎ x χ

Proof

Step Hyp Ref Expression
1 albid.1 ⊢ Ⅎ x φ
2 albid.2 ⊢ φ → ψ ↔ χ
3 1 2 exbid ⊢ φ → ∃ x ψ ↔ ∃ x χ
4 1 2 albid ⊢ φ → ∀ x ψ ↔ ∀ x χ
5 3 4 imbi12d ⊢ φ → ∃ x ψ → ∀ x ψ ↔ ∃ x χ → ∀ x χ
6 df-nf ⊢ Ⅎ x ψ ↔ ∃ x ψ → ∀ x ψ
7 df-nf ⊢ Ⅎ x χ ↔ ∃ x χ → ∀ x χ
8 5 6 7 3bitr4g ⊢ φ → Ⅎ x ψ ↔ Ⅎ x χ