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

Theorem rexnal 2912
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 2911 . 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 2814   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  dfral2OLD  2914  rexanaliOLD  2967  2ralor  3031  elpwunsn  4068  uni0b  4270  iundif2  4392  weniso  6238  rexrnmpt2  6402  onnseq  7015  ixp0  7502  boxcutc  7512  isfinite2  7778  ordtypelem9  7951  ordtypelem10  7952  unbndrank  8260  tcrank  8302  infxpenlem  8391  kmlem3  8532  kmlem7  8536  kmlem8  8537  kmlem13  8542  cfeq0  8636  isf32lem2  8734  isf32lem5  8737  isf34lem4  8757  fin1a2lem7  8786  ac6n  8865  alephval2  8947  pwfseqlem3  9038  inttsk  9152  nqereu  9307  npomex  9374  prlem934  9411  arch  10792  qextlt  11402  qextle  11403  xralrple  11404  xrsupsslem  11498  xrinfmsslem  11499  supxrbnd1  11513  supxrbnd2  11514  supxrbnd  11520  fsuppmapnn0fiubex  12066  hashfun  12461  hashge2el2dif  12487  limsuplt  13265  alzdvds  13895  isprm5  14112  pc2dvds  14261  vdwnn  14375  ramcl  14406  cshwshashlem1  14438  cshwshash  14447  lt6abl  16700  mdetunilem8  18916  fctop  19299  cctop  19301  t0dist  19620  ist0-3  19640  pthaus  19902  txkgen  19916  xkohaus  19917  fbfinnfr  20105  isufil2  20172  hausflim  20245  fclscf  20289  bcth  21531  minveclem3b  21606  pmltpc  21625  volsup  21729  volsup2  21777  itg2seq  21912  itg2cn  21933  tdeglem4  22221  aaliou3lem9  22508  ftalem7  23108  dchrptlem3  23297  dchrsum2  23299  tglowdim1i  23648  tgdim01  23654  tglowdim2ln  23773  brbtwn2  23912  colinearalg  23917  axlowdimlem6  23954  axlowdimlem14  23962  usgra2edg1  24087  frgra2v  24703  4cycl2vnunb  24721  vdn0frgrav2  24728  vdgn0frgrav2  24729  nmounbi  25395  nmobndseqi  25398  minvecolem5  25501  xrnarchi  27418  isarchi2  27419  archiabl  27432  ordtconlem1  27570  lmdvg  27599  hasheuni  27759  voliune  27869  volfiniune  27870  ballotlemodife  28104  ballotlem4  28105  nodenselem4  29049  nodenselem5  29050  nofulllem5  29071  tfrqfree  29206  brub  29209  mblfinlem1  29656  nn0prpw  29746  filnetlem4  29830  smprngopr  30080  fphpd  30382  fiphp3d  30385  rencldnfilem  30386  pellfundglb  30453  rexnal2  31033  limcrecl  31199  stoweidlem14  31342  stoweidlem34  31362  usg2edgneu  31907  pgrpgt2nabl  32056  islindeps  32153  islininds2  32184  ldepslinc  32209  bnj1542  33012  bnj110  33013  bnj1189  33162
  Copyright terms: Public domain W3C validator