Users' Mathboxes 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 35498
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 35491 and bj-exlimg 35495 (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
StepHypRef Expression
1 19.38 1841 . 2 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
2 bj-alrimg 35491 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
3 bj-exlimg 35495 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
42, 3jaoi 855 . 2 (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
51, 4impbid2 225 1 (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wo 845  wal 1539  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 206  df-or 846  df-ex 1782
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator