Theorem rexnal 1210

Description: Relationship between restricted universal and existential quantifiers.

Assertion

Ref	Expression
rexnal	⊢ (∃x ∈ A ¬ φ ↔ ¬ ∀x ∈ A φ)

Proof of Theorem rexnal

Step	Hyp	Ref	Expression
1		exanali 725	. 2 ⊢ (∃x(x ∈ A ∧ ¬ φ) ↔ ¬ ∀x(x ∈ A → φ))
2		df-rex 1206	. 2 ⊢ (∃x ∈ A ¬ φ ↔ ∃x(x ∈ A ∧ ¬ φ))
3		df-ral 1205	. . 3 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
4	3	negbii 162	. 2 ⊢ (¬ ∀x ∈ A φ ↔ ¬ ∀x(x ∈ A → φ))
5	1, 2, 4	3bitr4 158	1 ⊢ (∃x ∈ A ¬ φ ↔ ¬ ∀x ∈ A φ)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202

This theorem is referenced by:  dfral2 1211  uni0b 1939  iundif2 2032  isfinite2 3437  unbndrank 3527  kmlem3 3582  kmlem7 3586  kmlem12 3591  kmlem13 3592  arch 4521  climunii 4883  infxpidmlem8 4940  hlimunii 5143

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-ral 1205  df-rex 1206

metamath.org