Definition df-exists-D5.1 596

Description: Definition of Existential Quantifier, '∃'. Read as "there exists".

Assertion

Ref	Expression
df-exists-D5.1	⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

Detailed syntax breakdown of Definition df-exists-D5.1

Step	Hyp	Ref	Expression
1		wff-ph	. . 3 wff 𝜑
2		objvar-x	. . 3 objvar 𝑥
3	1, 2	wff-exists 595	. 2 wff ∃𝑥𝜑
4	1	wff-neg 9	. . . 4 wff ¬ 𝜑
5	4, 2	wff-forall 8	. . 3 wff ∀𝑥 ¬ 𝜑
6	5	wff-neg 9	. 2 wff ¬ ∀𝑥 ¬ 𝜑
7	3, 6	wff-bi 104	1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

This definition is referenced by:  allnegex-P5  597  exnegall-P5  598  lemma-L5.01a  600  axL6ex-P5  625  cbvexv-P5  660  exiw-P5  662  genex-P6  731  cbvex-P6  752  psubex2v-P6  797  nfrexgencl-L6  813