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

Theorem ralnex 2427
 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 2422 . 2 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝜑))
2 alinexa 1583 . . 3 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥𝐴𝜑))
3 df-rex 2423 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
42, 3xchbinxr 673 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥𝐴 𝜑)
51, 4bitri 183 1 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1330  ∃wex 1469   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418 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 604  ax-in2 605  ax-5 1424  ax-gen 1426  ax-ie2 1471 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-fal 1338  df-ral 2422  df-rex 2423 This theorem is referenced by:  nnral  2429  rexalim  2432  ralinexa  2466  nrex  2528  nrexdv  2529  ralnex2  2575  uni0b  3770  iindif2m  3889  f0rn0  5326  supmoti  6890  fodjuomnilemdc  7026  ismkvnex  7039  suprnubex  8755  icc0r  9759  ioo0  10088  ico0  10090  ioc0  10091  prmind2  11857  sqrt2irr  11896  nconstwlpolem  13453
 Copyright terms: Public domain W3C validator