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

Theorem ralnex 2365
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 2360 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝜑))
2 alinexa 1537 . . 3 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 2361 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 641 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 182 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wal 1285  wex 1424  wcel 1436  wral 2355  wrex 2356
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-5 1379  ax-gen 1381  ax-ie2 1426
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-fal 1293  df-ral 2360  df-rex 2361
This theorem is referenced by:  rexalim  2369  ralinexa  2401  nrex  2461  nrexdv  2462  uni0b  3661  iindif2m  3780  f0rn0  5168  supmoti  6632  fodjuomnilemdc  6743  suprnubex  8349  icc0r  9276  ioo0  9599  ico0  9601  ioc0  9602  prmind2  10977  sqrt2irr  11016
  Copyright terms: Public domain W3C validator