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

Theorem rexnal 2708
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 2703 . 2  |-  ( E. x  e.  A  -.  ph  <->  E. x ( x  e.  A  /\  -.  ph ) )
2 exanali 1595 . . 3  |-  ( E. x ( x  e.  A  /\  -.  ph ) 
<->  -.  A. x ( x  e.  A  ->  ph ) )
3 df-ral 2702 . . 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 1549   E.wex 1550    e. wcel 1725   A.wral 2697   E.wrex 2698
This theorem is referenced by:  dfral2  2709  rexanali  2743  2ralor  2869  uni0b  4032  iundif2  4150  elpwunsn  4749  weniso  6067  rexrnmpt2  6177  onnseq  6598  ixp0  7087  boxcutc  7097  isfinite2  7357  ordtypelem9  7487  ordtypelem10  7488  unbndrank  7760  tcrank  7800  infxpenlem  7887  kmlem3  8024  kmlem7  8028  kmlem8  8029  kmlem13  8034  cfeq0  8128  isf32lem2  8226  isf32lem5  8229  isf34lem4  8249  fin1a2lem7  8278  ac6n  8357  alephval2  8439  pwfseqlem3  8527  inttsk  8641  nqereu  8798  npomex  8865  prlem934  8902  arch  10210  qextlt  10781  qextle  10782  xralrple  10783  xrsupsslem  10877  xrinfmsslem  10878  supxrbnd1  10892  supxrbnd2  10893  supxrbnd  10899  hashfun  11692  limsuplt  12265  alzdvds  12891  isprm5  13104  pc2dvds  13244  vdwnn  13358  ramcl  13389  lt6abl  15496  fctop  17060  cctop  17062  t0dist  17381  ist0-3  17401  pthaus  17662  txkgen  17676  xkohaus  17677  fbfinnfr  17865  isufil2  17932  hausflim  18005  fclscf  18049  bcth  19274  minveclem3b  19321  pmltpc  19339  volsup  19442  volsup2  19489  itg2seq  19626  itg2cn  19647  tdeglem4  19975  aaliou3lem9  20259  ftalem7  20853  dchrptlem3  21042  dchrsum2  21044  usgra2edg1  21395  nmounbi  22269  nmobndseqi  22272  minvecolem5  22375  xrnarchi  24246  isarchi2  24247  lmdvg  24330  hasheuni  24467  voliune  24577  volfiniune  24578  ballotlemodife  24747  ballotlem4  24748  nodenselem4  25631  nodenselem5  25632  nofulllem5  25653  tfrqfree  25788  brub  25791  brbtwn2  25836  colinearalg  25841  axlowdimlem6  25878  axlowdimlem14  25886  mblfinlem  26234  nn0prpw  26317  filnetlem4  26401  smprngopr  26653  fphpd  26868  fiphp3d  26871  rencldnfilem  26872  pellfundglb  26939  stoweidlem14  27730  stoweidlem34  27750  cshwssizelem1a  28242  cshwssizelem3  28245  cshwssize  28253  frgra2v  28326  4cycl2vnunb  28344  vdn0frgrav2  28351  vdgn0frgrav2  28352  bnj1542  29165  bnj110  29166  bnj1189  29315
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator