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

Theorem rexnal 2567
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 2562 . 2  |-  ( E. x  e.  A  -.  ph  <->  E. x ( x  e.  A  /\  -.  ph ) )
2 exanali 1575 . . 3  |-  ( E. x ( x  e.  A  /\  -.  ph ) 
<->  -.  A. x ( x  e.  A  ->  ph ) )
3 df-ral 2561 . . 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 1530   E.wex 1531    e. wcel 1696   A.wral 2556   E.wrex 2557
This theorem is referenced by:  dfral2  2568  rexanali  2602  2ralor  2722  uni0b  3868  iundif2  3985  elpwunsn  4584  weniso  5868  rexrnmpt2  5975  onnseq  6377  ixp0  6865  boxcutc  6875  isfinite2  7131  ordtypelem9  7257  ordtypelem10  7258  unbndrank  7530  tcrank  7570  infxpenlem  7657  kmlem3  7794  kmlem7  7798  kmlem8  7799  kmlem13  7804  cfeq0  7898  isf32lem2  7996  isf32lem5  7999  isf34lem4  8019  fin1a2lem7  8048  ac6n  8128  alephval2  8210  pwfseqlem3  8298  inttsk  8412  nqereu  8569  npomex  8636  prlem934  8673  arch  9978  qextlt  10546  qextle  10547  xralrple  10548  xrsupsslem  10641  xrinfmsslem  10642  supxrbnd1  10656  supxrbnd2  10657  supxrbnd  10663  hashfun  11405  limsuplt  11969  alzdvds  12594  isprm5  12807  pc2dvds  12947  vdwnn  13061  ramcl  13092  lt6abl  15197  fctop  16757  cctop  16759  t0dist  17069  ist0-3  17089  pthaus  17348  txkgen  17362  xkohaus  17363  fbfinnfr  17552  isufil2  17619  hausflim  17692  fclscf  17736  bcth  18767  minveclem3b  18808  pmltpc  18826  volsup  18929  volsup2  18976  itg2seq  19113  itg2cn  19134  tdeglem4  19462  aaliou3lem9  19746  ftalem7  20332  dchrptlem3  20521  dchrsum2  20523  nmounbi  21370  nmobndseqi  21373  minvecolem5  21476  ballotlemodife  23072  ballotlem4  23073  lmdvg  23391  hasheuni  23468  nodenselem4  24409  nodenselem5  24410  nofulllem5  24431  tfrqfree  24561  brbtwn2  24605  colinearalg  24610  axlowdimlem6  24647  axlowdimlem14  24655  negcmpprcal2  25049  fordisxex  25057  dstr  25274  iintlem1  25713  lvsovso2  25730  supnuf  25732  supexr  25734  nn0prpw  26342  filnetlem4  26433  smprngopr  26780  fphpd  27002  fiphp3d  27005  rencldnfilem  27006  pellfundglb  27073  stoweidlem14  27866  stoweidlem34  27886  frgra2v  28423  4cycl2vnunb  28439  bnj1542  29205  bnj110  29206  bnj1189  29355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator