Theorem bj-exnalimn 31797

Description: A transformation of quantifiers and logical connectives. The general statement that equs3 1862 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 1827. I propose to move to the main part: bj-exnalimn 31797, bj-exaleximi 31800, bj-exalimi 31801, bj-ax12i 31803, bj-ax12wlem 31807, bj-ax12w 31852, and remove equs3 1862. A new label is needed for bj-ax12i 31803 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1863 and spimfw 1865 (other spim* theorems use ∃𝑥 and very 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 1759	. 2 ⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓))
2	1	con2bii 346	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥(𝜑 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by: (None)