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 36608
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 1835) and the converse implication is the join of instances of bj-alrimg 36601 and bj-exlimg 36605 (see 19.38a 1836 and 19.38b 1837). 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 1835 . 2 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
2 bj-alrimg 36601 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
3 bj-exlimg 36605 . . 3 ((∃𝑥𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
42, 3jaoi 857 . 2 (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)))
51, 4impbid2 226 1 (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wo 847  wal 1534  wex 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805
This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1776
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator