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  3938  iindif2m  4058  f0rn0  5561  supmoti  7283  fodjuomnilemdc  7434  ismkvnex  7445  nninfwlpoimlemginf  7466  suprnubex  9226  icc0r  10258  ioo0  10618  ico0  10620  ioc0  10621  prmind2  12813  sqrt2irr  12855  umgrnloop0  16104  vtxd0nedgbfi  16286  1hevtxdg0fi  16294  nconstwlpolem  16842