Theorem bj-exnalimn 32610

Description: A transformation of quantifiers and logical connectives. The general statement that equs3 1875 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 1839. I propose to move to the main part: bj-exnalimn 32610, bj-exalim 32611, bj-exalimi 32612, bj-exalims 32613, bj-exalimsi 32614, bj-ax12i 32616, bj-ax12wlem 32617, bj-ax12w 32665, and remove equs3 1875. A new label is needed for bj-ax12i 32616 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1876 and spimfw 1878 (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

Step	Hyp	Ref	Expression
1		alinexa 1770	. 2 ⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓))
2	1	con2bii 347	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥(𝜑 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by: (None)