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

Theorem dfrex2 3202
 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 3199 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
21con2bii 361 1 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3106  ∃wrex 3107 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 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112 This theorem is referenced by:  rexim  3204  rexanali  3224  r19.23v  3238  nfrexd  3266  nfrexdg  3267  cbvrexfw  3384  cbvrexf  3386  rspcimedv  3562  sbcrext  3802  cbvrexcsf  3871  rabn0  4293  r19.9rzv  4403  rexxfrd  5276  rexxfr2d  5278  rexxfrd2  5280  rexxfr  5283  rexiunxp  5676  rexxpf  5683  rexrnmptw  6839  rexrnmpt  6841  cbvexfo  7025  rexrnmpo  7271  tz7.49  8067  dfsup2  8895  supnub  8913  infnlb  8943  wofib  8996  zfregs2  9162  alephval3  9524  ac6n  9899  prmreclem5  16249  sylow1lem3  18721  ordtrest2lem  21818  trfil2  22502  alexsubALTlem3  22664  alexsubALTlem4  22665  evth  23574  lhop1lem  24626  vdn0conngrumgrv2  27991  nmobndseqi  28572  chpssati  30156  chrelat3  30164  nn0min  30572  xrnarchi  30873  0nellinds  30996  ordtrest2NEWlem  31290  dffr5  33117  nosupbnd1lem4  33339  poimirlem1  35077  poimirlem26  35102  poimirlem27  35103  fdc  35202  lpssat  36328  lssat  36331  lfl1  36385  atlrelat1  36636  unxpwdom3  40082  ss2iundf  40403  zfregs2VD  41590
 Copyright terms: Public domain W3C validator