Theorem rexnal 2995

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

Step	Hyp	Ref	Expression
1		dfral2 2994	. 2 |- ( A. x e. A ph <-> -. E. x e. A -. ph )
2	1	con2bii 347	1 |- ( E. x e. A -. ph <-> -. A. x e. A ph )

Syntax hints:   -. wn 3   <-> wb 196   A.wral 2912   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexnal2  3043  rexnal3  3044  2ralor  3109  elpwunsn  4224  n0snor2el  4364  uni0b  4463  iundif2  4587  weniso  6604  rexrnmpt2  6776  onnseq  7441  ixp0  7941  boxcutc  7951  isfinite2  8218  ordtypelem9  8431  ordtypelem10  8432  unbndrank  8705  tcrank  8747  infxpenlem  8836  kmlem3  8974  kmlem7  8978  kmlem8  8979  kmlem13  8984  cfeq0  9078  isf32lem2  9176  isf32lem5  9179  isf34lem4  9199  fin1a2lem7  9228  ac6n  9307  alephval2  9394  pwfseqlem3  9482  inttsk  9596  nqereu  9751  npomex  9818  prlem934  9855  arch  11289  qextlt  12034  qextle  12035  xralrple  12036  xrsupsslem  12137  xrinfmsslem  12138  supxrbnd1  12151  supxrbnd2  12152  supxrbnd  12158  fsuppmapnn0fiubex  12792  hashfun  13224  hashge2el2dif  13262  limsuplt  14210  fprodle  14727  alzdvds  15042  isprm5  15419  ncoprmlnprm  15436  pc2dvds  15583  vdwnn  15702  ramcl  15733  cshwshashlem1  15802  cshwshash  15811  isnsgrp  17288  isnmnd  17298  lt6abl  18296  mdetunilem8  20425  fctop  20808  cctop  20810  t0dist  21129  ist0-3  21149  pthaus  21441  txkgen  21455  xkohaus  21456  fbfinnfr  21645  isufil2  21712  hausflim  21785  fclscf  21829  bcth  23126  minveclem3b  23199  pmltpc  23219  volsup  23324  volsup2  23373  itg2seq  23509  itg2cn  23530  tdeglem4  23820  aaliou3lem9  24105  ftalem7  24805  dchrptlem3  24991  dchrsum2  24993  tglowdim1i  25396  tgdim01  25402  tglowdim2ln  25546  brbtwn2  25785  colinearalg  25790  axlowdimlem6  25827  axlowdimlem14  25835  umgr2edg1  26103  umgr2edgneu  26106  nfrgr2v  27136  4cycl2vnunb  27154  nmounbi  27631  nmobndseqi  27634  minvecolem5  27737  fprodex01  29571  xrnarchi  29738  isarchi2  29739  ordtconnlem1  29970  lmdvg  29999  hasheuni  30147  voliune  30292  volfiniune  30293  ballotlemodife  30559  ballotlem4  30560  reprdifc  30705  bnj1542  30927  bnj110  30928  bnj1189  31077  noseponlem  31817  nolt02o  31845  noetalem3  31865  dfrecs2  32057  brub  32061  filnetlem4  32376  unblimceq0  32498  relowlpssretop  33212  matunitlindflem1  33405  poimirlem23  33432  poimirlem30  33439  poimirlem32  33441  poimir  33442  mblfinlem1  33446  fphpd  37380  fiphp3d  37383  rencldnfilem  37384  pellfundglb  37449  clsk3nimkb  38338  ndisj2  39218  eliin2f  39287  infrpge  39567  infxrbnd2  39585  supminfxr  39694  limcrecl  39861  limsupub  39936  limsuppnflem  39942  limsupre2lem  39956  stoweidlem14  40231  stoweidlem34  40251  salexct  40552  vonioo  40896  vonicc  40899  copisnmnd  41809  zrninitoringc  42071  pgrpgt2nabl  42147  islindeps  42242  islininds2  42273  ldepslinc  42298