Theorem dfrex2 3090

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.)

Assertion

Ref	Expression
dfrex2	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Proof of Theorem dfrex2

Step	Hyp	Ref	Expression
1		ralnex 3089	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
2	1	con2bii 360	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3077  ∃wrex 3087

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  rexanali  3117  r19.23v  3190  nfrexdw  3309  cbvrexf  3347  nfrexd  3359  rspcimedv  3568  rexab  3653  sbcrext  3820  cbvrexcsf  3890  rabn0  4339  rexn0  4452  r19.9rzv  4461  rexsng  4637  rexxfrd  5371  rexxfr2d  5373  rexxfrd2  5375  rexxfr  5378  rexiunxp  5817  rexxpf  5825  rexrnmptw  7087  rexrnmpt  7089  rexima  7236  cbvexfo  7290  rexrnmpo  7552  tz7.49  8439  dfsup2  9420  supnub  9438  infnlb  9469  wofib  9523  zfregs2  9718  alephval3  10170  ac6n  10544  prmreclem5  17078  sylow1lem3  19794  ordtrest2lem  23501  trfil2  24186  alexsubALTlem3  24348  alexsubALTlem4  24349  evth  25260  lhop1lem  26313  nosupbnd1lem4  28050  vdn0conngrumgrv2  30779  nmobndseqi  31363  chpssati  32947  chrelat3  32955  nn0min  33394  xrnarchi  33727  0nellinds  33908  ordtrest2NEWlem  34536  dffr5  36488  poimirlem1  38507  poimirlem26  38532  poimirlem27  38533  fdc  38647  lpssat  40038  lssat  40041  lfl1  40095  atlrelat1  40346  unxpwdom3  44055  onsupeqnmax  44207  sucomisnotcard  44503  ss2iundf  44618  zfregs2VD  45782  rext0  45880