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

Theorem dfrex2 2993
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 2989 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
21con2bii 347 1 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wral 2909  wrex 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-ral 2914  df-rex 2915
This theorem is referenced by:  rexanali  2995  nfrexd  3003  rexim  3005  r19.23v  3019  r19.30  3077  r19.35  3079  cbvrexf  3161  rspcimedv  3306  sbcrext  3505  sbcrextOLD  3506  cbvrexcsf  3559  rabn0  3949  r19.9rzv  4056  rexxfrd  4872  rexxfr2d  4874  rexxfrd2  4876  rexxfr  4879  rexiunxp  5251  rexxpf  5258  rexrnmpt  6355  cbvexfo  6530  rexrnmpt2  6761  tz7.49  7525  dfsup2  8335  supnub  8353  infnlb  8383  wofib  8435  zfregs2  8594  alephval3  8918  ac6n  9292  prmreclem5  15605  sylow1lem3  17996  ordtrest2lem  20988  trfil2  21672  alexsubALTlem3  21834  alexsubALTlem4  21835  evth  22739  lhop1lem  23757  vdn0conngrumgrv2  27036  nmobndseqi  27604  chpssati  29192  chrelat3  29200  nn0min  29541  xrnarchi  29712  ordtrest2NEWlem  29942  dffr5  31618  nosupbnd1lem4  31831  poimirlem1  33381  poimirlem26  33406  poimirlem27  33407  fdc  33512  lpssat  34119  lssat  34122  lfl1  34176  atlrelat1  34427  unxpwdom3  37484  ss2iundf  37770  zfregs2VD  38896
  Copyright terms: Public domain W3C validator