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 3052  ∃wrex 3061

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

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

This theorem is referenced by:  rexanali  3092  r19.23v  3169  nfrexdw  3294  cbvrexf  3345  nfrexd  3357  rspcimedv  3597  rexab  3683  sbcrext  3853  cbvrexcsf  3922  rabn0  4369  r19.9rzv  4480  rexn0  4491  rexsng  4657  rexxfrd  5384  rexxfr2d  5386  rexxfrd2  5388  rexxfr  5391  rexiunxp  5825  rexxpf  5832  rexrnmptw  7090  rexrnmpt  7092  rexima  7235  cbvexfo  7288  rexrnmpo  7552  tz7.49  8464  dfsup2  9461  supnub  9479  infnlb  9510  wofib  9564  zfregs2  9752  alephval3  10129  ac6n  10504  prmreclem5  16945  sylow1lem3  19586  ordtrest2lem  23146  trfil2  23830  alexsubALTlem3  23992  alexsubALTlem4  23993  evth  24914  lhop1lem  25975  nosupbnd1lem4  27680  vdn0conngrumgrv2  30182  nmobndseqi  30765  chpssati  32349  chrelat3  32357  nn0min  32804  xrnarchi  33187  0nellinds  33390  ordtrest2NEWlem  33958  dffr5  35776  poimirlem1  37650  poimirlem26  37675  poimirlem27  37676  fdc  37774  lpssat  39036  lssat  39039  lfl1  39093  atlrelat1  39344  unxpwdom3  43086  onsupeqnmax  43238  sucomisnotcard  43535  ss2iundf  43650  zfregs2VD  44832  rext0  44930