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