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

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

Proof of Theorem rexnal
StepHypRef Expression
1 notnot 291 . . . 4  |-  ( ph  <->  -. 
-.  ph )
21ralbii 2836 . . 3  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  -.  -.  ph )
3 ralnex 2848 . . 3  |-  ( A. x  e.  A  -.  -.  ph  <->  -.  E. x  e.  A  -.  ph )
42, 3bitri 249 . 2  |-  ( A. x  e.  A  ph  <->  -.  E. x  e.  A  -.  ph )
54con2bii 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 2796   E.wrex 2797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-ral 2801  df-rex 2802
This theorem is referenced by:  dfral2  2851  rexanali  2877  2ralor  2990  elpwunsn  4020  uni0b  4219  iundif2  4340  weniso  6149  rexrnmpt2  6311  onnseq  6910  ixp0  7401  boxcutc  7411  isfinite2  7676  ordtypelem9  7846  ordtypelem10  7847  unbndrank  8155  tcrank  8197  infxpenlem  8286  kmlem3  8427  kmlem7  8431  kmlem8  8432  kmlem13  8437  cfeq0  8531  isf32lem2  8629  isf32lem5  8632  isf34lem4  8652  fin1a2lem7  8681  ac6n  8760  alephval2  8842  pwfseqlem3  8933  inttsk  9047  nqereu  9204  npomex  9271  prlem934  9308  arch  10682  qextlt  11279  qextle  11280  xralrple  11281  xrsupsslem  11375  xrinfmsslem  11376  supxrbnd1  11390  supxrbnd2  11391  supxrbnd  11397  hashge2el2dif  12297  hashfun  12312  limsuplt  13070  alzdvds  13696  isprm5  13911  pc2dvds  14058  vdwnn  14172  ramcl  14203  cshwshashlem1  14235  cshwshash  14244  lt6abl  16487  mdetunilem8  18552  fctop  18735  cctop  18737  t0dist  19056  ist0-3  19076  pthaus  19338  txkgen  19352  xkohaus  19353  fbfinnfr  19541  isufil2  19608  hausflim  19681  fclscf  19725  bcth  20967  minveclem3b  21042  pmltpc  21061  volsup  21165  volsup2  21213  itg2seq  21348  itg2cn  21369  tdeglem4  21657  aaliou3lem9  21944  ftalem7  22544  dchrptlem3  22733  dchrsum2  22735  tglowdim1i  23084  tgdim01  23090  tglowdim2ln  23191  brbtwn2  23298  colinearalg  23303  axlowdimlem6  23340  axlowdimlem14  23348  usgra2edg1  23449  nmounbi  24323  nmobndseqi  24326  minvecolem5  24429  xrnarchi  26341  isarchi2  26342  archiabl  26355  ordtconlem1  26494  lmdvg  26523  hasheuni  26674  voliune  26784  volfiniune  26785  ballotlemodife  27019  ballotlem4  27020  nodenselem4  27964  nodenselem5  27965  nofulllem5  27986  tfrqfree  28121  brub  28124  mblfinlem1  28571  nn0prpw  28661  filnetlem4  28745  smprngopr  28995  fphpd  29298  fiphp3d  29301  rencldnfilem  29302  pellfundglb  29369  stoweidlem14  29952  stoweidlem34  29972  frgra2v  30734  4cycl2vnunb  30752  vdn0frgrav2  30759  vdgn0frgrav2  30760  pgrpgt2nabel  30914  fsuppmapnn0fiubex  30943  islindeps  31101  islininds2  31132  ldepslinc  31165  bnj1542  32163  bnj110  32164  bnj1189  32313
  Copyright terms: Public domain W3C validator