Theorem bj-nfimexal 35503

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 1842) and the converse implication is the join of instances of bj-alrimg 35496 and bj-exlimg 35500 (see 19.38a 1843 and 19.38b 1844). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.)

Assertion

Ref	Expression
bj-nfimexal	⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))

Proof of Theorem bj-nfimexal

Step	Hyp	Ref	Expression
1		19.38 1842	. 2 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
2		bj-alrimg 35496	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
3		bj-exlimg 35500	. . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
4	2, 3	jaoi 856	. 2 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
5	1, 4	impbid2 225	1 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 846  ∀wal 1540  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812

This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783

This theorem is referenced by: (None)