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

Theorem ralnex 2458
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 2453 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝜑))
2 alinexa 1596 . . 3 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 2454 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 678 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 183 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wal 1346  wex 1485  wcel 2141  wral 2448  wrex 2449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ie2 1487
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-fal 1354  df-ral 2453  df-rex 2454
This theorem is referenced by:  nnral  2460  rexalim  2463  ralinexa  2497  nrex  2562  nrexdv  2563  ralnex2  2609  r19.30dc  2617  uni0b  3821  iindif2m  3940  f0rn0  5392  supmoti  6970  fodjuomnilemdc  7120  ismkvnex  7131  nninfwlpoimlemginf  7152  suprnubex  8869  icc0r  9883  ioo0  10216  ico0  10218  ioc0  10219  prmind2  12074  sqrt2irr  12116  nconstwlpolem  14096
  Copyright terms: Public domain W3C validator