Theorem rexnal 2905

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

Proof of Theorem rexnal

Step	Hyp	Ref	Expression
1		dfral2 2904	. 2
2	1	con2bii 332	1

Syntax hints:  -.wn 3  <->wb 184  A.wral 2807  E.wrex 2808

This theorem is referenced by:  dfral2OLD  2907  rexnal2  2961  rexanaliOLD  2962  2ralor  3027  elpwunsn  4070  uni0b  4274  iundif2  4397  weniso  6250  rexrnmpt2  6418  onnseq  7034  ixp0  7522  boxcutc  7532  isfinite2  7798  ordtypelem9  7972  ordtypelem10  7973  unbndrank  8281  tcrank  8323  infxpenlem  8412  kmlem3  8553  kmlem7  8557  kmlem8  8558  kmlem13  8563  cfeq0  8657  isf32lem2  8755  isf32lem5  8758  isf34lem4  8778  fin1a2lem7  8807  ac6n  8886  alephval2  8968  pwfseqlem3  9059  inttsk  9173  nqereu  9328  npomex  9395  prlem934  9432  arch  10817  qextlt  11431  qextle  11432  xralrple  11433  xrsupsslem  11527  xrinfmsslem  11528  supxrbnd1  11542  supxrbnd2  11543  supxrbnd  11549  fsuppmapnn0fiubex  12098  hashfun  12495  hashge2el2dif  12521  limsuplt  13302  alzdvds  14036  isprm5  14253  pc2dvds  14402  vdwnn  14516  ramcl  14547  cshwshashlem1  14580  cshwshash  14589  isnsgrp  15915  isnmnd  15924  lt6abl  16897  mdetunilem8  19121  fctop  19505  cctop  19507  t0dist  19826  ist0-3  19846  pthaus  20139  txkgen  20153  xkohaus  20154  fbfinnfr  20342  isufil2  20409  hausflim  20482  fclscf  20526  bcth  21768  minveclem3b  21843  pmltpc  21862  volsup  21966  volsup2  22014  itg2seq  22149  itg2cn  22170  tdeglem4  22458  aaliou3lem9  22746  ftalem7  23352  dchrptlem3  23541  dchrsum2  23543  tglowdim1i  23892  tgdim01  23898  tglowdim2ln  24032  brbtwn2  24208  colinearalg  24213  axlowdimlem6  24250  axlowdimlem14  24258  usgra2edg1  24383  frgra2v  24999  4cycl2vnunb  25017  vdn0frgrav2  25023  vdgn0frgrav2  25024  nmounbi  25691  nmobndseqi  25694  minvecolem5  25797  xrnarchi  27728  isarchi2  27729  ordtconlem1  27906  lmdvg  27935  hasheuni  28091  voliune  28201  volfiniune  28202  ballotlemodife  28436  ballotlem4  28437  nodenselem4  29444  nodenselem5  29445  nofulllem5  29466  tfrqfree  29601  brub  29604  mblfinlem1  30051  filnetlem4  30199  fphpd  30750  fiphp3d  30753  rencldnfilem  30754  pellfundglb  30821  fprodle  31604  limcrecl  31635  stoweidlem14  31796  stoweidlem34  31816  usg2edgneu  32412  copisnmnd  32497  zrninitoringc  32879  pgrpgt2nabl  32959  islindeps  33054  islininds2  33085  ldepslinc  33110  bnj1542  33915  bnj110  33916  bnj1189  34065

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813