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

Theorem dfrex2 3073
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 3072 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
21con2bii 358 1 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3062  df-rex 3071
This theorem is referenced by:  rexanali  3102  rexbiOLD  3105  r19.23v  3176  nfrexdw  3292  cbvrexf  3333  nfrexd  3345  rspcimedv  3571  rexab  3653  sbcrext  3830  cbvrexcsf  3902  rabn0  4346  r19.9rzv  4458  rexn0  4469  rexsng  4636  rexxfrd  5365  rexxfr2d  5367  rexxfrd2  5369  rexxfr  5372  rexiunxp  5797  rexxpf  5804  rexrnmptw  7046  rexrnmpt  7048  cbvexfo  7237  rexrnmpo  7496  tz7.49  8392  dfsup2  9385  supnub  9403  infnlb  9433  wofib  9486  zfregs2  9674  alephval3  10051  ac6n  10426  prmreclem5  16797  sylow1lem3  19387  ordtrest2lem  22570  trfil2  23254  alexsubALTlem3  23416  alexsubALTlem4  23417  evth  24338  lhop1lem  25393  nosupbnd1lem4  27075  vdn0conngrumgrv2  29182  nmobndseqi  29763  chpssati  31347  chrelat3  31355  nn0min  31765  xrnarchi  32069  0nellinds  32206  ordtrest2NEWlem  32560  dffr5  34383  poimirlem1  36125  poimirlem26  36150  poimirlem27  36151  fdc  36250  lpssat  37521  lssat  37524  lfl1  37578  atlrelat1  37829  unxpwdom3  41465  onsupeqnmax  41624  sucomisnotcard  41904  ss2iundf  42019  zfregs2VD  43211
  Copyright terms: Public domain W3C validator