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

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

Proof of Theorem dfral2
StepHypRef Expression
1 notnotb 304 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21ralbii 3009 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 ¬ ¬ 𝜑)
3 ralnex 3021 . 2 (∀𝑥𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
42, 3bitri 264 1 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wral 2941  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  rexnal  3024  boxcutc  7993  infssuni  8298  ac6n  9345  indstr  11794  trfil3  21739  tglowdim2ln  25591  nmobndseqi  27762  stri  29244  hstri  29252  reprinfz1  30828  bnj1204  31206  nosepon  31943  poimirlem1  33540  n0elqs  34239
  Copyright terms: Public domain W3C validator