Metamath Proof Explorer

Theorem bj-nfimexal

Description: A weak from of nonfreeness in either an antecedent or a consequent implies that a universally quantified implication is equivalent to the associated implication where the antecedent is existentially quantified and the consequent is universally quantified. The forward implication always holds (this is 19.38 ) and the converse implication is the join of instances of bj-alrimg and bj-exlimg (see 19.38a and 19.38b ). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023)

Ref Expression
Assertion bj-nfimexal ⊢ ∃ x φ → ∀ x φ ∨ ∃ x ψ → ∀ x ψ → ∃ x φ → ∀ x ψ ↔ ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 19.38 ⊢ ∃ x φ → ∀ x ψ → ∀ x φ → ψ
2 bj-alrimg ⊢ ∃ x φ → ∀ x φ → ∀ x φ → ψ → ∃ x φ → ∀ x ψ
3 bj-exlimg ⊢ ∃ x ψ → ∀ x ψ → ∀ x φ → ψ → ∃ x φ → ∀ x ψ
4 2 3 jaoi ⊢ ∃ x φ → ∀ x φ ∨ ∃ x ψ → ∀ x ψ → ∀ x φ → ψ → ∃ x φ → ∀ x ψ
5 1 4 impbid2 ⊢ ∃ x φ → ∀ x φ ∨ ∃ x ψ → ∀ x ψ → ∃ x φ → ∀ x ψ ↔ ∀ x φ → ψ