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

Theorem rexnal 3204
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 3203 . 2 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
21con2bii 361 1 (∃𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wral 3109  wrex 3110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3114  df-rex 3115
This theorem is referenced by:  rexnal2  3222  rexnal3  3223  r19.35  3298  2ralor  3325  elpwunsn  4584  n0snor2el  4727  uni0b  4829  iundif2  4962  weniso  7090  rexrnmpo  7273  onnseq  7968  ixp0  8482  boxcutc  8492  isfinite2  8764  ordtypelem9  8978  ordtypelem10  8979  unbndrank  9259  tcrank  9301  infxpenlem  9428  kmlem3  9567  kmlem7  9571  kmlem8  9572  kmlem13  9577  cfeq0  9671  isf32lem2  9769  isf32lem5  9772  isf34lem4  9792  fin1a2lem7  9821  ac6n  9900  alephval2  9987  pwfseqlem3  10075  inttsk  10189  nqereu  10344  npomex  10411  prlem934  10448  arch  11886  qextlt  12588  qextle  12589  xralrple  12590  xrsupsslem  12692  xrinfmsslem  12693  supxrbnd1  12706  supxrbnd2  12707  supxrbnd  12713  fsuppmapnn0fiubex  13359  hashfun  13798  hashge2el2dif  13838  limsuplt  14832  fprodle  15346  alzdvds  15666  isprm5  16045  ncoprmlnprm  16062  pc2dvds  16209  vdwnn  16328  ramcl  16359  cshwshashlem1  16425  cshwshash  16434  isnsgrp  17901  isnmnd  17911  smndex1n0mnd  18073  lt6abl  19012  simpgnideld  19218  mdetunilem8  21228  fctop  21613  cctop  21615  t0dist  21934  ist0-3  21954  pthaus  22247  txkgen  22261  xkohaus  22262  fbfinnfr  22450  isufil2  22517  hausflim  22590  fclscf  22634  bcth  23937  minveclem3b  24036  pmltpc  24058  volsup  24164  volsup2  24213  itg2seq  24350  itg2cn  24371  tdeglem4  24665  aaliou3lem9  24950  ftalem7  25668  dchrptlem3  25854  dchrsum2  25856  tglowdim1i  26299  tglowdim2ln  26449  brbtwn2  26703  colinearalg  26708  axlowdimlem6  26745  axlowdimlem14  26753  umgr2edg1  27005  umgr2edgneu  27008  nfrgr2v  28061  4cycl2vnunb  28079  nmounbi  28563  nmobndseqi  28566  minvecolem5  28668  fprodex01  30571  xrnarchi  30867  isarchi2  30868  ssmxidllem  31053  fedgmullem2  31118  ordtconnlem1  31281  lmdvg  31310  hasheuni  31458  voliune  31602  volfiniune  31603  ballotlemodife  31869  ballotlem4  31870  reprdifc  32012  bnj1542  32243  bnj110  32244  bnj1189  32395  noseponlem  33285  nolt02o  33313  noetalem3  33333  dfrecs2  33525  brub  33529  filnetlem4  33843  unblimceq0  33960  relowlpssretop  34782  nlpineqsn  34826  matunitlindflem1  35052  poimirlem23  35079  poimirlem30  35086  poimirlem32  35088  poimir  35089  mblfinlem1  35093  dffltz  39608  fphpd  39750  fiphp3d  39753  rencldnfilem  39754  pellfundglb  39819  clsk3nimkb  40736  ndisj2  41678  eliin2f  41733  infrpge  41976  infxrbnd2  41994  supminfxr  42096  limcrecl  42264  limsupub  42339  limsuppnflem  42345  limsupre2lem  42359  stoweidlem14  42649  stoweidlem34  42669  salexct  42967  meaiuninc3v  43116  vonioo  43314  vonicc  43317  copisnmnd  44422  zrninitoringc  44688  pgrpgt2nabl  44761  islindeps  44855  islininds2  44886  ldepslinc  44911  line2ylem  45158  line2xlem  45160
  Copyright terms: Public domain W3C validator