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

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

Proof of Theorem dfral2
StepHypRef Expression
1 notnotb 316 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21ralbii 3162 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 ¬ ¬ 𝜑)
3 ralnex 3233 . 2 (∀𝑥𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
42, 3bitri 276 1 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wral 3135  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3140  df-rex 3141
This theorem is referenced by:  rexnal  3235  boxcutc  8493  infssuni  8803  ac6n  9895  indstr  12304  trfil3  22424  tglowdim2ln  26364  nmobndseqi  28483  stri  29961  hstri  29969  reprinfz1  31792  bnj1204  32181  nosepon  33069  fvineqsneq  34575  poimirlem1  34774  n0elqs  35464
  Copyright terms: Public domain W3C validator