Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-nfimexal Structured version   Visualization version   GIF version

Theorem bj-nfimexal 34073
 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 1840) and the converse implication is the join of instances of bj-alrimg 34066 and bj-exlimg 34070 (see 19.38a 1841 and 19.38b 1842). 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
StepHypRef Expression
1 19.38 1840 . 2 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
2 bj-alrimg 34066 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
3 bj-exlimg 34070 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
42, 3jaoi 854 . 2 (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
51, 4impbid2 229 1 (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 844  ∀wal 1536  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator