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

Theorem dfrex2 3236
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 3233 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
21con2bii 359 1 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wral 3135  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3140  df-rex 3141
This theorem is referenced by:  rexim  3238  rexanali  3262  r19.23v  3276  nfrexd  3304  nfrexdg  3305  r19.30OLD  3336  cbvrexfw  3436  cbvrexf  3438  rspcimedv  3611  sbcrext  3853  cbvrexcsf  3923  rabn0  4336  r19.9rzv  4441  rexxfrd  5300  rexxfr2d  5302  rexxfrd2  5304  rexxfr  5307  rexiunxp  5704  rexxpf  5711  rexrnmptw  6853  rexrnmpt  6855  cbvexfo  7037  rexrnmpo  7279  tz7.49  8070  dfsup2  8896  supnub  8914  infnlb  8944  wofib  8997  zfregs2  9163  alephval3  9524  ac6n  9895  prmreclem5  16244  sylow1lem3  18654  ordtrest2lem  21739  trfil2  22423  alexsubALTlem3  22585  alexsubALTlem4  22586  evth  23490  lhop1lem  24537  vdn0conngrumgrv2  27902  nmobndseqi  28483  chpssati  30067  chrelat3  30075  nn0min  30463  xrnarchi  30740  0nellinds  30862  ordtrest2NEWlem  31064  dffr5  32886  nosupbnd1lem4  33108  poimirlem1  34774  poimirlem26  34799  poimirlem27  34800  fdc  34901  lpssat  36029  lssat  36032  lfl1  36086  atlrelat1  36337  unxpwdom3  39573  ss2iundf  39882  zfregs2VD  41052
  Copyright terms: Public domain W3C validator