Theorem ralnex 2496

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 2491	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑))
2		alinexa 1627	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 2492	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 685	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 184	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1371  ∃wex 1516   ∈ wcel 2178  ∀wral 2486  ∃wrex 2487

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 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-ie2 1518

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-fal 1379  df-ral 2491  df-rex 2492

This theorem is referenced by:  nnral  2498  rexalim  2501  ralinexa  2535  nrex  2600  nrexdv  2601  ralnex2  2647  r19.30dc  2655  uni0b  3889  iindif2m  4009  f0rn0  5492  supmoti  7121  fodjuomnilemdc  7272  ismkvnex  7283  nninfwlpoimlemginf  7304  suprnubex  9061  icc0r  10083  ioo0  10439  ico0  10441  ioc0  10442  prmind2  12557  sqrt2irr  12599  nconstwlpolem  16206