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

Theorem rexnal 3024
 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
StepHypRef Expression
1 dfral2 3023 . 2 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
21con2bii 346 1 (∃𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wral 2941  ∃wrex 2942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947 This theorem is referenced by:  rexnal2  3072  rexnal3  3073  2ralor  3138  elpwunsn  4256  n0snor2el  4396  uni0b  4495  iundif2  4619  weniso  6644  rexrnmpt2  6818  onnseq  7486  ixp0  7983  boxcutc  7993  isfinite2  8259  ordtypelem9  8472  ordtypelem10  8473  unbndrank  8743  tcrank  8785  infxpenlem  8874  kmlem3  9012  kmlem7  9016  kmlem8  9017  kmlem13  9022  cfeq0  9116  isf32lem2  9214  isf32lem5  9217  isf34lem4  9237  fin1a2lem7  9266  ac6n  9345  alephval2  9432  pwfseqlem3  9520  inttsk  9634  nqereu  9789  npomex  9856  prlem934  9893  arch  11327  qextlt  12072  qextle  12073  xralrple  12074  xrsupsslem  12175  xrinfmsslem  12176  supxrbnd1  12189  supxrbnd2  12190  supxrbnd  12196  fsuppmapnn0fiubex  12832  hashfun  13262  hashge2el2dif  13300  limsuplt  14254  fprodle  14771  alzdvds  15089  isprm5  15466  ncoprmlnprm  15483  pc2dvds  15630  vdwnn  15749  ramcl  15780  cshwshashlem1  15849  cshwshash  15858  isnsgrp  17335  isnmnd  17345  lt6abl  18342  mdetunilem8  20473  fctop  20856  cctop  20858  t0dist  21177  ist0-3  21197  pthaus  21489  txkgen  21503  xkohaus  21504  fbfinnfr  21692  isufil2  21759  hausflim  21832  fclscf  21876  bcth  23172  minveclem3b  23245  pmltpc  23265  volsup  23370  volsup2  23419  itg2seq  23554  itg2cn  23575  tdeglem4  23865  aaliou3lem9  24150  ftalem7  24850  dchrptlem3  25036  dchrsum2  25038  tglowdim1i  25441  tgdim01  25447  tglowdim2ln  25591  brbtwn2  25830  colinearalg  25835  axlowdimlem6  25872  axlowdimlem14  25880  umgr2edg1  26148  umgr2edgneu  26151  nfrgr2v  27252  4cycl2vnunb  27270  nmounbi  27759  nmobndseqi  27762  minvecolem5  27865  fprodex01  29699  xrnarchi  29866  isarchi2  29867  ordtconnlem1  30098  lmdvg  30127  hasheuni  30275  voliune  30420  volfiniune  30421  ballotlemodife  30687  ballotlem4  30688  reprdifc  30833  bnj1542  31053  bnj110  31054  bnj1189  31203  noseponlem  31942  nolt02o  31970  noetalem3  31990  dfrecs2  32182  brub  32186  filnetlem4  32501  unblimceq0  32623  relowlpssretop  33342  matunitlindflem1  33535  poimirlem23  33562  poimirlem30  33569  poimirlem32  33571  poimir  33572  mblfinlem1  33576  fphpd  37697  fiphp3d  37700  rencldnfilem  37701  pellfundglb  37766  clsk3nimkb  38655  ndisj2  39532  eliin2f  39601  infrpge  39880  infxrbnd2  39898  supminfxr  40007  limcrecl  40179  limsupub  40254  limsuppnflem  40260  limsupre2lem  40274  stoweidlem14  40549  stoweidlem34  40569  salexct  40870  meaiuninc3v  41019  vonioo  41217  vonicc  41220  copisnmnd  42134  zrninitoringc  42396  pgrpgt2nabl  42472  islindeps  42567  islininds2  42598  ldepslinc  42623
 Copyright terms: Public domain W3C validator