MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfrex2 Structured version   Visualization version   GIF version

Theorem dfrex2 3142
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
StepHypRef Expression
1 ralnex 3139 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
21con2bii 348 1 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wral 3055  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061
This theorem is referenced by:  rexanali  3144  nfrexd  3152  rexim  3154  r19.23v  3170  r19.30  3229  r19.35  3231  cbvrexf  3314  rspcimedv  3463  sbcrext  3670  cbvrexcsf  3724  rabn0  4122  r19.9rzv  4224  rexxfrd  5044  rexxfr2d  5046  rexxfrd2  5048  rexxfr  5051  rexiunxp  5431  rexxpf  5438  rexrnmpt  6559  cbvexfo  6737  rexrnmpt2  6974  tz7.49  7744  dfsup2  8557  supnub  8575  infnlb  8605  wofib  8657  zfregs2  8824  alephval3  9184  ac6n  9560  prmreclem5  15905  sylow1lem3  18281  ordtrest2lem  21287  trfil2  21970  alexsubALTlem3  22132  alexsubALTlem4  22133  evth  23037  lhop1lem  24067  vdn0conngrumgrv2  27432  nmobndseqi  28025  chpssati  29613  chrelat3  29621  nn0min  29951  xrnarchi  30120  ordtrest2NEWlem  30350  dffr5  32020  nosupbnd1lem4  32233  poimirlem1  33766  poimirlem26  33791  poimirlem27  33792  fdc  33895  lpssat  34901  lssat  34904  lfl1  34958  atlrelat1  35209  unxpwdom3  38274  ss2iundf  38558  zfregs2VD  39661
  Copyright terms: Public domain W3C validator