Theorem dfrex2 3064

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3051  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3052  df-rex 3062

This theorem is referenced by:  rexanali  3091  r19.23v  3164  nfrexdw  3283  cbvrexf  3323  nfrexd  3335  rspcimedv  3555  rexab  3641  sbcrext  3811  cbvrexcsf  3880  rabn0  4329  rexn0  4436  r19.9rzv  4445  rexsng  4620  rexxfrd  5351  rexxfr2d  5353  rexxfrd2  5355  rexxfr  5358  rexiunxp  5795  rexxpf  5802  rexrnmptw  7047  rexrnmpt  7049  rexima  7193  cbvexfo  7245  rexrnmpo  7507  tz7.49  8384  dfsup2  9357  supnub  9375  infnlb  9406  wofib  9460  zfregs2  9654  alephval3  10032  ac6n  10407  prmreclem5  16891  sylow1lem3  19575  ordtrest2lem  23168  trfil2  23852  alexsubALTlem3  24014  alexsubALTlem4  24015  evth  24926  lhop1lem  25980  nosupbnd1lem4  27675  vdn0conngrumgrv2  30266  nmobndseqi  30850  chpssati  32434  chrelat3  32442  nn0min  32894  xrnarchi  33245  0nellinds  33430  ordtrest2NEWlem  34066  dffr5  35936  poimirlem1  37942  poimirlem26  37967  poimirlem27  37968  fdc  38066  lpssat  39459  lssat  39462  lfl1  39516  atlrelat1  39767  unxpwdom3  43523  onsupeqnmax  43675  sucomisnotcard  43971  ss2iundf  44086  zfregs2VD  45267  rext0  45365