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

Theorem rexnal 2716
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 2711 . 2  |-  ( E. x  e.  A  -.  ph  <->  E. x ( x  e.  A  /\  -.  ph ) )
2 exanali 1637 . . 3  |-  ( E. x ( x  e.  A  /\  -.  ph ) 
<->  -.  A. x ( x  e.  A  ->  ph ) )
3 df-ral 2710 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
42, 3xchbinxr 311 . 2  |-  ( E. x ( x  e.  A  /\  -.  ph ) 
<->  -.  A. x  e.  A  ph )
51, 4bitri 249 1  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1360   E.wex 1589    e. wcel 1755   A.wral 2705   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-ral 2710  df-rex 2711
This theorem is referenced by:  dfral2  2717  rexanali  2751  2ralor  2880  elpwunsn  3905  uni0b  4104  iundif2  4225  weniso  6032  rexrnmpt2  6195  onnseq  6791  ixp0  7284  boxcutc  7294  isfinite2  7558  ordtypelem9  7728  ordtypelem10  7729  unbndrank  8037  tcrank  8079  infxpenlem  8168  kmlem3  8309  kmlem7  8313  kmlem8  8314  kmlem13  8319  cfeq0  8413  isf32lem2  8511  isf32lem5  8514  isf34lem4  8534  fin1a2lem7  8563  ac6n  8642  alephval2  8724  pwfseqlem3  8814  inttsk  8928  nqereu  9085  npomex  9152  prlem934  9189  arch  10563  qextlt  11160  qextle  11161  xralrple  11162  xrsupsslem  11256  xrinfmsslem  11257  supxrbnd1  11271  supxrbnd2  11272  supxrbnd  11278  hashge2el2dif  12167  hashfun  12182  limsuplt  12940  alzdvds  13565  isprm5  13780  pc2dvds  13927  vdwnn  14041  ramcl  14072  cshwshashlem1  14104  cshwshash  14113  lt6abl  16350  mdetunilem8  18266  fctop  18449  cctop  18451  t0dist  18770  ist0-3  18790  pthaus  19052  txkgen  19066  xkohaus  19067  fbfinnfr  19255  isufil2  19322  hausflim  19395  fclscf  19439  bcth  20681  minveclem3b  20756  pmltpc  20775  volsup  20878  volsup2  20926  itg2seq  21061  itg2cn  21082  tdeglem4  21413  aaliou3lem9  21700  ftalem7  22300  dchrptlem3  22489  dchrsum2  22491  tglowdim1i  22835  brbtwn2  22973  colinearalg  22978  axlowdimlem6  23015  axlowdimlem14  23023  usgra2edg1  23124  nmounbi  23998  nmobndseqi  24001  minvecolem5  24104  xrnarchi  26024  isarchi2  26025  archiabl  26038  ordtconlem1  26207  lmdvg  26236  hasheuni  26387  voliune  26498  volfiniune  26499  ballotlemodife  26727  ballotlem4  26728  nodenselem4  27671  nodenselem5  27672  nofulllem5  27693  tfrqfree  27828  brub  27831  mblfinlem1  28269  nn0prpw  28359  filnetlem4  28443  smprngopr  28693  fphpd  28997  fiphp3d  29000  rencldnfilem  29001  pellfundglb  29068  stoweidlem14  29652  stoweidlem34  29672  frgra2v  30434  4cycl2vnunb  30452  vdn0frgrav2  30459  vdgn0frgrav2  30460  pgrpgt2nabel  30597  islindeps  30693  islininds2  30724  ldepslinc  30757  bnj1542  31549  bnj110  31550  bnj1189  31699
  Copyright terms: Public domain W3C validator