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

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
StepHypRef Expression
1 ralnex 3073 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
21con2bii 357 1 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
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 1797  ax-4 1811
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3063  df-rex 3072
This theorem is referenced by:  rexanali  3103  rexbiOLD  3106  r19.23v  3177  nfrexdw  3291  cbvrexf  3332  nfrexd  3344  rspcimedv  3570  rexab  3650  sbcrext  3827  cbvrexcsf  3899  rabn0  4343  r19.9rzv  4455  rexn0  4466  rexsng  4633  rexxfrd  5362  rexxfr2d  5364  rexxfrd2  5366  rexxfr  5369  rexiunxp  5794  rexxpf  5801  rexrnmptw  7041  rexrnmpt  7043  cbvexfo  7232  rexrnmpo  7489  tz7.49  8383  dfsup2  9338  supnub  9356  infnlb  9386  wofib  9439  zfregs2  9627  alephval3  10004  ac6n  10379  prmreclem5  16746  sylow1lem3  19335  ordtrest2lem  22500  trfil2  23184  alexsubALTlem3  23346  alexsubALTlem4  23347  evth  24268  lhop1lem  25323  nosupbnd1lem4  27005  vdn0conngrumgrv2  28985  nmobndseqi  29566  chpssati  31150  chrelat3  31158  nn0min  31558  xrnarchi  31862  0nellinds  32001  ordtrest2NEWlem  32331  dffr5  34159  poimirlem1  36011  poimirlem26  36036  poimirlem27  36037  fdc  36136  lpssat  37407  lssat  37410  lfl1  37464  atlrelat1  37715  unxpwdom3  41325  onsupeqnmax  41484  sucomisnotcard  41721  ss2iundf  41836  zfregs2VD  43028
  Copyright terms: Public domain W3C validator