Theorem bj-nfimexal 34807

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 1841) and the converse implication is the join of instances of bj-alrimg 34800 and bj-exlimg 34804 (see 19.38a 1842 and 19.38b 1843). 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 1841	. 2 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
2		bj-alrimg 34800	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
3		bj-exlimg 34804	. . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
4	2, 3	jaoi 854	. 2 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
5	1, 4	impbid2 225	1 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 844  ∀wal 1537  ∃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 845  df-ex 1783

This theorem is referenced by: (None)