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

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

Proof of Theorem dfral2
StepHypRef Expression
1 notnotb 319 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21ralbii 3098 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 ¬ ¬ 𝜑)
3 ralnex 3164 . 2 (∀𝑥𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
42, 3bitri 278 1 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3071  ∃wrex 3072 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 210  df-an 401  df-ex 1783  df-ral 3076  df-rex 3077 This theorem is referenced by:  rexnal  3166  boxcutc  8524  infssuni  8841  ac6n  9938  indstr  12349  trfil3  22581  tglowdim2ln  26537  nmobndseqi  28654  stri  30132  hstri  30140  reprinfz1  32114  bnj1204  32505  nosepon  33426  noinfbnd1lem4  33487  fvineqsneq  35102  poimirlem1  35331  n0elqs  36016
 Copyright terms: Public domain W3C validator