Theorem rexnal 1657

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 1045	. 2 ⊢ (∃x(x ∈ A ⋀ ¬ φ) ↔ ¬ ∀x(x ∈ A → φ))
2		df-rex 1653	. 2 ⊢ (∃x ∈ A ¬ φ ↔ ∃x(x ∈ A ⋀ ¬ φ))
3		df-ral 1652	. . 3 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
4	3	negbii 187	. 2 ⊢ (¬ ∀x ∈ A φ ↔ ¬ ∀x(x ∈ A → φ))
5	1, 2, 4	3bitr4 183	1 ⊢ (∃x ∈ A ¬ φ ↔ ¬ ∀x ∈ A φ)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 956   ∈ wcel 960  ∃wex 982  ∀wral 1648  ∃wrex 1649

This theorem is referenced by:  dfral2 1658  rexanali 1687  uni0b 2527  iundif2 2615  elpwunsn 2918  ixp0 4367  isfinite2 4557  isfinite2OLD 4558  unbndrank 4693  ac6n 4767  kmlem3 4777  kmlem7 4781  kmlem8 4782  kmlem13 4787  alephval2 4913  cfeq0 4926  arch 6073  xrsupsslem 6078  xrinfmsslem 6079  supxrbnd 6093  supxrbnd1 6097  supxrbnd2 6098  climunii 7098  climubi 7153  infxpidmlem8 7560  fctopOLD 7647  cctop 7649  bcthlem33 8028  nmounbi 8435  hlimunii 9103  nmcopexlem1 9946  nmcfnexlem1 9975  iintlem1 10603

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-ral 1652  df-rex 1653

Copyright terms: Public domain