NFE Home 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