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

Theorem dfral2 3097
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 3098. (Revised by Wolf Lammen, 9-Dec-2019.)
Assertion
Ref Expression
dfral2 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)

Proof of Theorem dfral2
StepHypRef Expression
1 notnotb 315 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21ralbii 3091 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 ¬ ¬ 𝜑)
3 ralnex 3070 . 2 (∀𝑥𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
42, 3bitri 275 1 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wral 3059  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069
This theorem is referenced by:  rexnal  3098  imaeqsalvOLD  7384  boxcutc  8980  infssuni  9384  ac6n  10523  indstr  12956  trfil3  23912  nosepon  27725  noinfbnd1lem4  27786  cuteq1  27893  tglowdim2ln  28674  nmobndseqi  30808  stri  32286  hstri  32294  reprinfz1  34616  bnj1204  35005  fvineqsneq  37395  poimirlem1  37608  n0elqs  38308
  Copyright terms: Public domain W3C validator