Theorem ralnex 2465

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1351  ∃wex 1492   ∈ wcel 2148  ∀wral 2455  ∃wrex 2456

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ie2 1494

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-fal 1359  df-ral 2460  df-rex 2461

This theorem is referenced by:  nnral  2467  rexalim  2470  ralinexa  2504  nrex  2569  nrexdv  2570  ralnex2  2616  r19.30dc  2624  uni0b  3836  iindif2m  3956  f0rn0  5412  supmoti  6995  fodjuomnilemdc  7145  ismkvnex  7156  nninfwlpoimlemginf  7177  suprnubex  8913  icc0r  9929  ioo0  10263  ico0  10265  ioc0  10266  prmind2  12123  sqrt2irr  12165  nconstwlpolem  14954