Theorem dfrex2 3074

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3062  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063  df-rex 3072

This theorem is referenced by:  rexanali  3103  rexbiOLD  3106  r19.23v  3183  nfrexdw  3308  cbvrexf  3358  nfrexd  3370  rspcimedv  3604  rexab  3691  sbcrext  3868  cbvrexcsf  3940  rabn0  4386  r19.9rzv  4500  rexn0  4511  rexsng  4679  rexxfrd  5408  rexxfr2d  5410  rexxfrd2  5412  rexxfr  5415  rexiunxp  5841  rexxpf  5848  rexrnmptw  7097  rexrnmpt  7099  cbvexfo  7288  rexrnmpo  7548  tz7.49  8445  dfsup2  9439  supnub  9457  infnlb  9487  wofib  9540  zfregs2  9728  alephval3  10105  ac6n  10480  prmreclem5  16853  sylow1lem3  19468  ordtrest2lem  22707  trfil2  23391  alexsubALTlem3  23553  alexsubALTlem4  23554  evth  24475  lhop1lem  25530  nosupbnd1lem4  27214  vdn0conngrumgrv2  29449  nmobndseqi  30032  chpssati  31616  chrelat3  31624  nn0min  32026  xrnarchi  32330  0nellinds  32483  ordtrest2NEWlem  32902  dffr5  34724  poimirlem1  36489  poimirlem26  36514  poimirlem27  36515  fdc  36613  lpssat  37883  lssat  37886  lfl1  37940  atlrelat1  38191  unxpwdom3  41837  onsupeqnmax  41996  sucomisnotcard  42295  ss2iundf  42410  zfregs2VD  43602