Theorem dfrex2 3065

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3052  ∃wrex 3062

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 3053  df-rex 3063

This theorem is referenced by:  rexanali  3092  r19.23v  3165  nfrexdw  3284  cbvrexf  3324  nfrexd  3336  rspcimedv  3556  rexab  3642  sbcrext  3812  cbvrexcsf  3881  rabn0  4330  rexn0  4437  r19.9rzv  4446  rexsng  4621  rexxfrd  5346  rexxfr2d  5348  rexxfrd2  5350  rexxfr  5353  rexiunxp  5789  rexxpf  5796  rexrnmptw  7041  rexrnmpt  7043  rexima  7186  cbvexfo  7238  rexrnmpo  7500  tz7.49  8377  dfsup2  9350  supnub  9368  infnlb  9399  wofib  9453  zfregs2  9645  alephval3  10023  ac6n  10398  prmreclem5  16882  sylow1lem3  19566  ordtrest2lem  23178  trfil2  23862  alexsubALTlem3  24024  alexsubALTlem4  24025  evth  24936  lhop1lem  25990  nosupbnd1lem4  27689  vdn0conngrumgrv2  30281  nmobndseqi  30865  chpssati  32449  chrelat3  32457  nn0min  32909  xrnarchi  33260  0nellinds  33445  ordtrest2NEWlem  34082  dffr5  35952  poimirlem1  37956  poimirlem26  37981  poimirlem27  37982  fdc  38080  lpssat  39473  lssat  39476  lfl1  39530  atlrelat1  39781  unxpwdom3  43541  onsupeqnmax  43693  sucomisnotcard  43989  ss2iundf  44104  zfregs2VD  45285  rext0  45383