Users' Mathboxes 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 32585
Description: A transformation of quantifiers and logical connectives. The general statement that equs3 1873 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 1837. I propose to move to the main part: bj-exnalimn 32585, bj-exalim 32586, bj-exalimi 32587, bj-exalims 32588, bj-exalimsi 32589, bj-ax12i 32591, bj-ax12wlem 32592, bj-ax12w 32640, and remove equs3 1873. A new label is needed for bj-ax12i 32591 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to 𝑥 in speimfw 1874 and spimfw 1876 (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 1768 . 2 (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑𝜓))
21con2bii 347 1 (∃𝑥(𝜑𝜓) ↔ ¬ ∀𝑥(𝜑 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1479  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator