Theorem ralnex 2400

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 2395	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑))
2		alinexa 1565	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 2396	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 655	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 183	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1312  ∃wex 1451   ∈ wcel 1463  ∀wral 2390  ∃wrex 2391

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-5 1406  ax-gen 1408  ax-ie2 1453

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-fal 1320  df-ral 2395  df-rex 2396

This theorem is referenced by:  rexalim  2404  ralinexa  2436  nrex  2498  nrexdv  2499  ralnex2  2545  uni0b  3727  iindif2m  3846  f0rn0  5275  supmoti  6832  fodjuomnilemdc  6966  ismkvnex  6979  suprnubex  8621  icc0r  9602  ioo0  9930  ico0  9932  ioc0  9933  prmind2  11647  sqrt2irr  11686