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

Theorem rexnal 2661
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 2656 . 2  |-  ( E. x  e.  A  -.  ph  <->  E. x ( x  e.  A  /\  -.  ph ) )
2 exanali 1592 . . 3  |-  ( E. x ( x  e.  A  /\  -.  ph ) 
<->  -.  A. x ( x  e.  A  ->  ph ) )
3 df-ral 2655 . . 3  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
42, 3xchbinxr 303 . 2  |-  ( E. x ( x  e.  A  /\  -.  ph ) 
<->  -.  A. x  e.  A  ph )
51, 4bitri 241 1  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546   E.wex 1547    e. wcel 1717   A.wral 2650   E.wrex 2651
This theorem is referenced by:  dfral2  2662  rexanali  2696  2ralor  2821  uni0b  3983  iundif2  4100  elpwunsn  4698  weniso  6015  rexrnmpt2  6125  onnseq  6543  ixp0  7032  boxcutc  7042  isfinite2  7302  ordtypelem9  7429  ordtypelem10  7430  unbndrank  7702  tcrank  7742  infxpenlem  7829  kmlem3  7966  kmlem7  7970  kmlem8  7971  kmlem13  7976  cfeq0  8070  isf32lem2  8168  isf32lem5  8171  isf34lem4  8191  fin1a2lem7  8220  ac6n  8299  alephval2  8381  pwfseqlem3  8469  inttsk  8583  nqereu  8740  npomex  8807  prlem934  8844  arch  10151  qextlt  10722  qextle  10723  xralrple  10724  xrsupsslem  10818  xrinfmsslem  10819  supxrbnd1  10833  supxrbnd2  10834  supxrbnd  10840  hashfun  11628  limsuplt  12201  alzdvds  12827  isprm5  13040  pc2dvds  13180  vdwnn  13294  ramcl  13325  lt6abl  15432  fctop  16992  cctop  16994  t0dist  17312  ist0-3  17332  pthaus  17592  txkgen  17606  xkohaus  17607  fbfinnfr  17795  isufil2  17862  hausflim  17935  fclscf  17979  bcth  19152  minveclem3b  19197  pmltpc  19215  volsup  19318  volsup2  19365  itg2seq  19502  itg2cn  19523  tdeglem4  19851  aaliou3lem9  20135  ftalem7  20729  dchrptlem3  20918  dchrsum2  20920  usgra2edg1  21270  nmounbi  22126  nmobndseqi  22129  minvecolem5  22232  lmdvg  24143  hasheuni  24272  voliune  24380  volfiniune  24381  ballotlemodife  24535  ballotlem4  24536  nodenselem4  25363  nodenselem5  25364  nofulllem5  25385  tfrqfree  25515  brbtwn2  25559  colinearalg  25564  axlowdimlem6  25601  axlowdimlem14  25609  nn0prpw  26018  filnetlem4  26102  smprngopr  26354  fphpd  26569  fiphp3d  26572  rencldnfilem  26573  pellfundglb  26640  stoweidlem14  27432  stoweidlem34  27452  frgra2v  27753  4cycl2vnunb  27771  vdn0frgrav2  27778  vdgn0frgrav2  27779  bnj1542  28567  bnj110  28568  bnj1189  28717
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-ral 2655  df-rex 2656
  Copyright terms: Public domain W3C validator