Theorem ralnex 2532

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 2527	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑))
2		alinexa 1652	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 2528	. . 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 2205  ∀wral 2522  ∃wrex 2523

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 2527  df-rex 2528

This theorem is referenced by:  nnral  2534  rexalim  2537  ralinexa  2571  nrex  2636  nrexdv  2637  ralnex2  2684  r19.30dc  2692  uni0b  3944  iindif2m  4064  f0rn0  5567  supmoti  7297  fodjuomnilemdc  7448  ismkvnex  7459  nninfwlpoimlemginf  7480  suprnubex  9244  icc0r  10278  ioo0  10643  ico0  10645  ioc0  10646  prmind2  12842  sqrt2irr  12884  umgrnloop0  16238  vtxd0nedgbfi  16420  1hevtxdg0fi  16428  nconstwlpolem  16977