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

Theorem rexnal 2889
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 9-Dec-2019.)
Assertion
Ref Expression
rexnal  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )

Proof of Theorem rexnal
StepHypRef Expression
1 dfral2 2888 . 2  |-  ( A. x  e.  A  ph  <->  -.  E. x  e.  A  -.  ph )
21con2bii 332 1  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   A.wral 2791   E.wrex 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-ral 2796  df-rex 2797
This theorem is referenced by:  dfral2OLD  2891  rexnal2  2945  rexanaliOLD  2946  2ralor  3011  elpwunsn  4051  uni0b  4255  iundif2  4378  weniso  6231  rexrnmpt2  6399  onnseq  7013  ixp0  7500  boxcutc  7510  isfinite2  7776  ordtypelem9  7949  ordtypelem10  7950  unbndrank  8258  tcrank  8300  infxpenlem  8389  kmlem3  8530  kmlem7  8534  kmlem8  8535  kmlem13  8540  cfeq0  8634  isf32lem2  8732  isf32lem5  8735  isf34lem4  8755  fin1a2lem7  8784  ac6n  8863  alephval2  8945  pwfseqlem3  9036  inttsk  9150  nqereu  9305  npomex  9372  prlem934  9409  arch  10793  qextlt  11406  qextle  11407  xralrple  11408  xrsupsslem  11502  xrinfmsslem  11503  supxrbnd1  11517  supxrbnd2  11518  supxrbnd  11524  fsuppmapnn0fiubex  12072  hashfun  12469  hashge2el2dif  12495  limsuplt  13276  alzdvds  13908  isprm5  14125  pc2dvds  14274  vdwnn  14388  ramcl  14419  cshwshashlem1  14452  cshwshash  14461  isnsgrp  15784  isnmnd  15793  lt6abl  16766  mdetunilem8  18988  fctop  19371  cctop  19373  t0dist  19692  ist0-3  19712  pthaus  20005  txkgen  20019  xkohaus  20020  fbfinnfr  20208  isufil2  20275  hausflim  20348  fclscf  20392  bcth  21634  minveclem3b  21709  pmltpc  21728  volsup  21832  volsup2  21880  itg2seq  22015  itg2cn  22036  tdeglem4  22324  aaliou3lem9  22611  ftalem7  23217  dchrptlem3  23406  dchrsum2  23408  tglowdim1i  23757  tgdim01  23763  tglowdim2ln  23897  brbtwn2  24073  colinearalg  24078  axlowdimlem6  24115  axlowdimlem14  24123  usgra2edg1  24248  frgra2v  24864  4cycl2vnunb  24882  vdn0frgrav2  24888  vdgn0frgrav2  24889  nmounbi  25556  nmobndseqi  25559  minvecolem5  25662  xrnarchi  27594  isarchi2  27595  ordtconlem1  27772  lmdvg  27801  hasheuni  27957  voliune  28067  volfiniune  28068  ballotlemodife  28302  ballotlem4  28303  nodenselem4  29412  nodenselem5  29413  nofulllem5  29434  tfrqfree  29569  brub  29572  mblfinlem1  30019  filnetlem4  30167  fphpd  30718  fiphp3d  30721  rencldnfilem  30722  pellfundglb  30789  limcrecl  31539  stoweidlem14  31681  stoweidlem34  31701  usg2edgneu  32246  copisnmnd  32330  pgrpgt2nabl  32667  islindeps  32764  islininds2  32795  ldepslinc  32820  bnj1542  33622  bnj110  33623  bnj1189  33772
  Copyright terms: Public domain W3C validator