New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  rexnal GIF version

Theorem rexnal 2625
 Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
Assertion
Ref Expression
rexnal (x A ¬ φ ↔ ¬ x A φ)

Proof of Theorem rexnal
StepHypRef Expression
1 df-rex 2620 . 2 (x A ¬ φx(x A ¬ φ))
2 exanali 1585 . . 3 (x(x A ¬ φ) ↔ ¬ x(x Aφ))
3 df-ral 2619 . . 3 (x A φx(x Aφ))
42, 3xchbinxr 302 . 2 (x(x A ¬ φ) ↔ ¬ x A φ)
51, 4bitri 240 1 (x A ¬ φ ↔ ¬ x A φ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   ∈ wcel 1710  ∀wral 2614  ∃wrex 2615 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-ral 2619  df-rex 2620 This theorem is referenced by:  dfral2  2626  rexanali  2660  2ralor  2780  uni0b  3916  iundif2  4033  dfint3  4318  dfnnc2  4395  nndisjeq  4429  ncfinraiselem2  4480  nnpweqlem1  4522  rexxpf  4828  transex  5910  refex  5911  antisymex  5912  connexex  5913  extex  5915  symex  5916  nchoicelem11  6299
 Copyright terms: Public domain W3C validator