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

Theorem bj-exnalimn 32735
 Description: A transformation of quantifiers and logical connectives. The general statement that equs3 1932 proves. This and the following theorems are the general instances of already proved theorems. They could be moved to the main part, before ax-5 1879. I propose to move to the main part: bj-exnalimn 32735, bj-exalim 32736, bj-exalimi 32737, bj-exalims 32738, bj-exalimsi 32739, bj-ax12i 32741, bj-ax12wlem 32742, bj-ax12w 32790, and remove equs3 1932. A new label is needed for bj-ax12i 32741 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1933 and spimfw 1935 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 29-Sep-2019.)
Assertion
Ref Expression
bj-exnalimn (∃𝑥(𝜑𝜓) ↔ ¬ ∀𝑥(𝜑 → ¬ 𝜓))

Proof of Theorem bj-exnalimn
StepHypRef Expression
1 alinexa 1810 . 2 (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑𝜓))
21con2bii 346 1 (∃𝑥(𝜑𝜓) ↔ ¬ ∀𝑥(𝜑 → ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521  ∃wex 1744 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator