Theorem bj-nfimexal 37093

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 1862) and the converse implication is the join of instances of bj-alrimg 37068 and bj-exlimg 37090 (see 19.38a 1863 and 19.38b 1864). 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 1862	. 2 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
2		bj-alrimg 37068	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
3		bj-exlimg 37090	. . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
4	2, 3	jaoi 870	. 2 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
5	1, 4	impbid2 229	1 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860  ∀wal 1561  ∃wex 1802

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

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1803

This theorem is referenced by: (None)