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

Theorem rexnal 3133
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 3132 . 2 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
21con2bii 346 1 (∃𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wral 3050  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-ral 3055  df-rex 3056
This theorem is referenced by:  rexnal2  3181  rexnal3  3182  2ralor  3247  elpwunsn  4368  n0snor2el  4509  uni0b  4615  iundif2  4739  weniso  6768  rexrnmpt2  6942  onnseq  7611  ixp0  8109  boxcutc  8119  isfinite2  8385  ordtypelem9  8598  ordtypelem10  8599  unbndrank  8880  tcrank  8922  infxpenlem  9046  kmlem3  9186  kmlem7  9190  kmlem8  9191  kmlem13  9196  cfeq0  9290  isf32lem2  9388  isf32lem5  9391  isf34lem4  9411  fin1a2lem7  9440  ac6n  9519  alephval2  9606  pwfseqlem3  9694  inttsk  9808  nqereu  9963  npomex  10030  prlem934  10067  arch  11501  qextlt  12247  qextle  12248  xralrple  12249  xrsupsslem  12350  xrinfmsslem  12351  supxrbnd1  12364  supxrbnd2  12365  supxrbnd  12371  fsuppmapnn0fiubex  13006  hashfun  13436  hashge2el2dif  13474  limsuplt  14429  fprodle  14946  alzdvds  15264  isprm5  15641  ncoprmlnprm  15658  pc2dvds  15805  vdwnn  15924  ramcl  15955  cshwshashlem1  16024  cshwshash  16033  isnsgrp  17509  isnmnd  17519  lt6abl  18516  mdetunilem8  20647  fctop  21030  cctop  21032  t0dist  21351  ist0-3  21371  pthaus  21663  txkgen  21677  xkohaus  21678  fbfinnfr  21866  isufil2  21933  hausflim  22006  fclscf  22050  bcth  23346  minveclem3b  23419  pmltpc  23439  volsup  23544  volsup2  23593  itg2seq  23728  itg2cn  23749  tdeglem4  24039  aaliou3lem9  24324  ftalem7  25025  dchrptlem3  25211  dchrsum2  25213  tglowdim1i  25616  tgdim01  25622  tglowdim2ln  25766  brbtwn2  26005  colinearalg  26010  axlowdimlem6  26047  axlowdimlem14  26055  umgr2edg1  26323  umgr2edgneu  26326  nfrgr2v  27447  4cycl2vnunb  27465  nmounbi  27961  nmobndseqi  27964  minvecolem5  28067  fprodex01  29901  xrnarchi  30068  isarchi2  30069  ordtconnlem1  30300  lmdvg  30329  hasheuni  30477  voliune  30622  volfiniune  30623  ballotlemodife  30889  ballotlem4  30890  reprdifc  31035  bnj1542  31255  bnj110  31256  bnj1189  31405  noseponlem  32144  nolt02o  32172  noetalem3  32192  dfrecs2  32384  brub  32388  filnetlem4  32703  unblimceq0  32825  relowlpssretop  33541  matunitlindflem1  33736  poimirlem23  33763  poimirlem30  33770  poimirlem32  33772  poimir  33773  mblfinlem1  33777  fphpd  37900  fiphp3d  37903  rencldnfilem  37904  pellfundglb  37969  clsk3nimkb  38858  ndisj2  39735  eliin2f  39804  infrpge  40083  infxrbnd2  40101  supminfxr  40210  limcrecl  40382  limsupub  40457  limsuppnflem  40463  limsupre2lem  40477  stoweidlem14  40752  stoweidlem34  40772  salexct  41073  meaiuninc3v  41222  vonioo  41420  vonicc  41423  copisnmnd  42337  zrninitoringc  42599  pgrpgt2nabl  42675  islindeps  42770  islininds2  42801  ldepslinc  42826
  Copyright terms: Public domain W3C validator