Theorem dfrex2 2979

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 2975	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
2	1	con2bii 346	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 195  ∀wral 2896  ∃wrex 2897

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  df-ral 2901  df-rex 2902

This theorem is referenced by:  rexanali  2981  nfrexd  2989  rexim  2991  r19.23v  3005  r19.30  3063  r19.35  3065  cbvrexf  3142  rspcimedv  3284  sbcrext  3478  sbcrextOLD  3479  cbvrexcsf  3532  rabn0  3912  r19.9rzv  4017  rexxfrd  4807  rexxfr2d  4809  rexxfrd2  4811  rexxfr  4814  rexiunxp  5184  rexxpf  5191  rexrnmpt  6277  cbvexfo  6445  rexrnmpt2  6674  tz7.49  7427  dfsup2  8233  supnub  8251  infnlb  8281  wofib  8333  zfregs2  8492  alephval3  8816  ac6n  9190  prmreclem5  15462  sylow1lem3  17838  ordtrest2lem  20817  trfil2  21501  alexsubALTlem3  21663  alexsubALTlem4  21664  evth  22566  lhop1lem  23580  nmobndseqi  27018  chpssati  28606  chrelat3  28614  nn0min  28954  xrnarchi  29069  ordtrest2NEWlem  29296  dffr5  30896  poimirlem1  32580  poimirlem26  32605  poimirlem27  32606  fdc  32711  lpssat  33318  lssat  33321  lfl1  33375  atlrelat1  33626  unxpwdom3  36683  ss2iundf  36970  zfregs2VD  38098  vdn0conngrumgrv2  41363