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

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

Proof of Theorem dfral2
StepHypRef Expression
1 notnotb 315 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21ralbii 3093 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 ¬ ¬ 𝜑)
3 ralnex 3072 . 2 (∀𝑥𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
42, 3bitri 275 1 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wral 3061  wrex 3070
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 3062  df-rex 3071
This theorem is referenced by:  rexnal  3100  imaeqsalv  7310  boxcutc  8882  infssuni  9290  ac6n  10426  indstr  12846  trfil3  23255  nosepon  27029  noinfbnd1lem4  27090  tglowdim2ln  27635  nmobndseqi  29763  stri  31241  hstri  31249  reprinfz1  33292  bnj1204  33681  fvineqsneq  35929  poimirlem1  36125  n0elqs  36833
  Copyright terms: Public domain W3C validator