MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexnal Unicode version

Theorem rexnal 2554
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
Assertion
Ref Expression
rexnal  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )

Proof of Theorem rexnal
StepHypRef Expression
1 df-rex 2549 . 2  |-  ( E. x  e.  A  -.  ph  <->  E. x ( x  e.  A  /\  -.  ph ) )
2 exanali 1572 . . 3  |-  ( E. x ( x  e.  A  /\  -.  ph ) 
<->  -.  A. x ( x  e.  A  ->  ph ) )
3 df-ral 2548 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
42, 3xchbinxr 302 . 2  |-  ( E. x ( x  e.  A  /\  -.  ph ) 
<->  -.  A. x  e.  A  ph )
51, 4bitri 240 1  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    e. wcel 1684   A.wral 2543   E.wrex 2544
This theorem is referenced by:  dfral2  2555  rexanali  2589  2ralor  2709  uni0b  3852  iundif2  3969  elpwunsn  4568  weniso  5852  rexrnmpt2  5959  onnseq  6361  ixp0  6849  boxcutc  6859  isfinite2  7115  ordtypelem9  7241  ordtypelem10  7242  unbndrank  7514  tcrank  7554  infxpenlem  7641  kmlem3  7778  kmlem7  7782  kmlem8  7783  kmlem13  7788  cfeq0  7882  isf32lem2  7980  isf32lem5  7983  isf34lem4  8003  fin1a2lem7  8032  ac6n  8112  alephval2  8194  pwfseqlem3  8282  inttsk  8396  nqereu  8553  npomex  8620  prlem934  8657  arch  9962  qextlt  10530  qextle  10531  xralrple  10532  xrsupsslem  10625  xrinfmsslem  10626  supxrbnd1  10640  supxrbnd2  10641  supxrbnd  10647  hashfun  11389  limsuplt  11953  alzdvds  12578  isprm5  12791  pc2dvds  12931  vdwnn  13045  ramcl  13076  lt6abl  15181  fctop  16741  cctop  16743  t0dist  17053  ist0-3  17073  pthaus  17332  txkgen  17346  xkohaus  17347  fbfinnfr  17536  isufil2  17603  hausflim  17676  fclscf  17720  bcth  18751  minveclem3b  18792  pmltpc  18810  volsup  18913  volsup2  18960  itg2seq  19097  itg2cn  19118  tdeglem4  19446  aaliou3lem9  19730  ftalem7  20316  dchrptlem3  20505  dchrsum2  20507  nmounbi  21354  nmobndseqi  21357  minvecolem5  21460  ballotlemodife  23056  ballotlem4  23057  lmdvg  23376  hasheuni  23453  nodenselem4  24338  nodenselem5  24339  nofulllem5  24360  tfrqfree  24489  brbtwn2  24533  colinearalg  24538  axlowdimlem6  24575  axlowdimlem14  24583  negcmpprcal2  24946  fordisxex  24954  dstr  25171  iintlem1  25610  lvsovso2  25627  supnuf  25629  supexr  25631  nn0prpw  26239  filnetlem4  26330  smprngopr  26677  fphpd  26899  fiphp3d  26902  rencldnfilem  26903  pellfundglb  26970  stoweidlem14  27763  stoweidlem34  27783  frgra2v  28177  bnj1542  28889  bnj110  28890  bnj1189  29039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator