Theorem ralnex 2530

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)

Assertion

Ref	Expression
ralnex	⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Proof of Theorem ralnex

Step	Hyp	Ref	Expression
1		df-ral 2525	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑))
2		alinexa 1652	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 2526	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 690	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 184	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1396  ∃wex 1541   ∈ wcel 2203  ∀wral 2520  ∃wrex 2521

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-ie2 1543

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-fal 1404  df-ral 2525  df-rex 2526

This theorem is referenced by:  nnral  2532  rexalim  2535  ralinexa  2569  nrex  2634  nrexdv  2635  ralnex2  2682  r19.30dc  2690  uni0b  3939  iindif2m  4059  f0rn0  5562  supmoti  7284  fodjuomnilemdc  7435  ismkvnex  7446  nninfwlpoimlemginf  7467  suprnubex  9227  icc0r  10259  ioo0  10619  ico0  10621  ioc0  10622  prmind2  12817  sqrt2irr  12859  umgrnloop0  16112  vtxd0nedgbfi  16294  1hevtxdg0fi  16302  nconstwlpolem  16851