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

Theorem ralnex 2400
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 2395 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝜑))
2 alinexa 1565 . . 3 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 2396 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 655 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 183 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wal 1312  wex 1451  wcel 1463  wral 2390  wrex 2391
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-5 1406  ax-gen 1408  ax-ie2 1453
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-fal 1320  df-ral 2395  df-rex 2396
This theorem is referenced by:  rexalim  2404  ralinexa  2436  nrex  2498  nrexdv  2499  ralnex2  2545  uni0b  3727  iindif2m  3846  f0rn0  5275  supmoti  6832  fodjuomnilemdc  6966  ismkvnex  6979  suprnubex  8621  icc0r  9602  ioo0  9930  ico0  9932  ioc0  9933  prmind2  11647  sqrt2irr  11686
  Copyright terms: Public domain W3C validator