ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralnex GIF version

Theorem ralnex 2482
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
Assertion
Ref Expression
ralnex (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)

Proof of Theorem ralnex
StepHypRef Expression
1 df-ral 2477 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝜑))
2 alinexa 1614 . . 3 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 2478 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 684 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 184 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wal 1362  wex 1503  wcel 2164  wral 2472  wrex 2473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-ie2 1505
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370  df-ral 2477  df-rex 2478
This theorem is referenced by:  nnral  2484  rexalim  2487  ralinexa  2521  nrex  2586  nrexdv  2587  ralnex2  2633  r19.30dc  2641  uni0b  3860  iindif2m  3980  f0rn0  5440  supmoti  7042  fodjuomnilemdc  7193  ismkvnex  7204  nninfwlpoimlemginf  7225  suprnubex  8962  icc0r  9982  ioo0  10318  ico0  10320  ioc0  10321  prmind2  12248  sqrt2irr  12290  nconstwlpolem  15500
  Copyright terms: Public domain W3C validator