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

Theorem rexnal 2991
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 2990 . 2 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
21con2bii 347 1 (∃𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wral 2908  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2913  df-rex 2914
This theorem is referenced by:  rexnal2  3038  rexnal3  3039  2ralor  3103  elpwunsn  4202  n0snor2el  4339  uni0b  4436  iundif2  4560  weniso  6569  rexrnmpt2  6741  onnseq  7401  ixp0  7901  boxcutc  7911  isfinite2  8178  ordtypelem9  8391  ordtypelem10  8392  unbndrank  8665  tcrank  8707  infxpenlem  8796  kmlem3  8934  kmlem7  8938  kmlem8  8939  kmlem13  8944  cfeq0  9038  isf32lem2  9136  isf32lem5  9139  isf34lem4  9159  fin1a2lem7  9188  ac6n  9267  alephval2  9354  pwfseqlem3  9442  inttsk  9556  nqereu  9711  npomex  9778  prlem934  9815  arch  11249  qextlt  11993  qextle  11994  xralrple  11995  xrsupsslem  12096  xrinfmsslem  12097  supxrbnd1  12110  supxrbnd2  12111  supxrbnd  12117  fsuppmapnn0fiubex  12748  hashfun  13180  hashge2el2dif  13216  limsuplt  14160  fprodle  14671  alzdvds  14985  isprm5  15362  ncoprmlnprm  15379  pc2dvds  15526  vdwnn  15645  ramcl  15676  cshwshashlem1  15745  cshwshash  15754  isnsgrp  17228  isnmnd  17238  lt6abl  18236  mdetunilem8  20365  fctop  20748  cctop  20750  t0dist  21069  ist0-3  21089  pthaus  21381  txkgen  21395  xkohaus  21396  fbfinnfr  21585  isufil2  21652  hausflim  21725  fclscf  21769  bcth  23066  minveclem3b  23139  pmltpc  23159  volsup  23264  volsup2  23313  itg2seq  23449  itg2cn  23470  tdeglem4  23758  aaliou3lem9  24043  ftalem7  24739  dchrptlem3  24925  dchrsum2  24927  tglowdim1i  25330  tgdim01  25336  tglowdim2ln  25480  brbtwn2  25719  colinearalg  25724  axlowdimlem6  25761  axlowdimlem14  25769  umgr2edg1  26030  umgr2edgneu  26033  nfrgr2v  27034  4cycl2vnunb  27052  nmounbi  27519  nmobndseqi  27522  minvecolem5  27625  xrnarchi  29565  isarchi2  29566  ordtconnlem1  29794  lmdvg  29823  hasheuni  29970  voliune  30115  volfiniune  30116  ballotlemodife  30382  ballotlem4  30383  bnj1542  30688  bnj110  30689  bnj1189  30838  noseponlem  31575  nodenselem4  31600  nodenselem5  31601  dfrecs2  31752  brub  31756  filnetlem4  32071  unblimceq0  32193  relowlpssretop  32883  matunitlindflem1  33076  poimirlem23  33103  poimirlem30  33110  poimirlem32  33112  poimir  33113  mblfinlem1  33117  fphpd  36899  fiphp3d  36902  rencldnfilem  36903  pellfundglb  36968  clsk3nimkb  37859  ndisj2  38740  eliin2f  38809  infrpge  39066  infxrbnd2  39084  limcrecl  39297  limsupub  39372  limsuppnflem  39378  limsupre2lem  39392  stoweidlem14  39568  stoweidlem34  39588  salexct  39889  vonioo  40233  vonicc  40236  copisnmnd  41127  zrninitoringc  41389  pgrpgt2nabl  41465  islindeps  41560  islininds2  41591  ldepslinc  41616
  Copyright terms: Public domain W3C validator