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

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

Proof of Theorem dfral2
StepHypRef Expression
1 notnotb 315 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21ralbii 3094 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 ¬ ¬ 𝜑)
3 ralnex 3073 . 2 (∀𝑥𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
42, 3bitri 275 1 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wral 3062  wrex 3071
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 3063  df-rex 3072
This theorem is referenced by:  rexnal  3101  imaeqsalv  7361  boxcutc  8935  infssuni  9343  ac6n  10480  indstr  12900  trfil3  23392  nosepon  27168  noinfbnd1lem4  27229  cuteq1  27334  tglowdim2ln  27902  nmobndseqi  30032  stri  31510  hstri  31518  reprinfz1  33634  bnj1204  34023  fvineqsneq  36293  poimirlem1  36489  n0elqs  37195
  Copyright terms: Public domain W3C validator