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

Metamath Proof Explorer

Theorem nfbidv

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 ⊢ φ → ψ ↔ χ
Assertion nfbidv ⊢ φ → Ⅎ x ψ ↔ Ⅎ x χ

Proof

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