Theorem nex 1833

Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)

Hypothesis

Ref	Expression
nex.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
nex	⊢ ¬ ∃𝑥𝜑

Proof of Theorem nex

Step	Hyp	Ref	Expression
1		alnex 1814	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		nex.1	. 2 ⊢ ¬ 𝜑
3	1, 2	mpgbi 1831	1 ⊢ ¬ ∃𝑥𝜑

This proof depends on syntax axioms:  ¬ wn 3  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  ru  3741  noel  4286  noelOLD  4287  uni0  4901  axnulALT  5264  vnex  5277  notsep  5332  dtrucor2  5341  opelopabsb  5511  0nelopab  5547  0nelxp  5692  0xp  5758  xp0  5759  cnv0  5873  cnv0OLD  5874  dm0  5914  co02  6283  dffv3  6912  mpo0  7536  canth2  9187  snnen2o  9274  1sdom2dom  9283  brdom3  10646  ruc  16455  join0  18627  meet0  18628  0g0  18894  ustn0  24595  bnj1523  35812  axnulALT2  35825  onf1oracwevd  36093  mirimanofffr  36670  linedegen  37123  nexntru  37407  nexfal  37408  unqsym1  37428  elttcirr  37534  bj-dtrucor2v  37944  bj-ru1  38071  bj-0nelsngl  38099  bj-ccinftydisj  38402  disjALTV0  40052  dtrucor3  50240