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

Theorem rexnal 2977
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 2976 . 2 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
21con2bii 345 1 (∃𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wral 2895  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  rexnal2  3024  rexnal3  3025  2ralor  3087  elpwunsn  4170  uni0b  4393  iundif2  4517  weniso  6482  rexrnmpt2  6652  onnseq  7306  ixp0  7805  boxcutc  7815  isfinite2  8081  ordtypelem9  8292  ordtypelem10  8293  unbndrank  8566  tcrank  8608  infxpenlem  8697  kmlem3  8835  kmlem7  8839  kmlem8  8840  kmlem13  8845  cfeq0  8939  isf32lem2  9037  isf32lem5  9040  isf34lem4  9060  fin1a2lem7  9089  ac6n  9168  alephval2  9251  pwfseqlem3  9339  inttsk  9453  nqereu  9608  npomex  9675  prlem934  9712  arch  11139  qextlt  11870  qextle  11871  xralrple  11872  xrsupsslem  11968  xrinfmsslem  11969  supxrbnd1  11982  supxrbnd2  11983  supxrbnd  11989  fsuppmapnn0fiubex  12612  hashfun  13039  hashge2el2dif  13070  limsuplt  14007  fprodle  14515  alzdvds  14829  isprm5  15206  ncoprmlnprm  15223  pc2dvds  15370  vdwnn  15489  ramcl  15520  cshwshashlem1  15589  cshwshash  15598  isnsgrp  17060  isnmnd  17070  lt6abl  18068  mdetunilem8  20192  fctop  20566  cctop  20568  t0dist  20887  ist0-3  20907  pthaus  21199  txkgen  21213  xkohaus  21214  fbfinnfr  21403  isufil2  21470  hausflim  21543  fclscf  21587  bcth  22879  minveclem3b  22952  pmltpc  22971  volsup  23076  volsup2  23124  itg2seq  23260  itg2cn  23281  tdeglem4  23569  aaliou3lem9  23854  ftalem7  24550  dchrptlem3  24736  dchrsum2  24738  tglowdim1i  25141  tgdim01  25147  tglowdim2ln  25292  brbtwn2  25531  colinearalg  25536  axlowdimlem6  25573  axlowdimlem14  25581  usgra2edg1  25706  frgra2v  26320  4cycl2vnunb  26338  vdn0frgrav2  26344  vdgn0frgrav2  26345  nmounbi  26849  nmobndseqi  26852  minvecolem5  26955  xrnarchi  28903  isarchi2  28904  ordtconlem1  29132  lmdvg  29161  hasheuni  29308  voliune  29453  volfiniune  29454  ballotlemodife  29720  ballotlem4  29721  bnj1542  30015  bnj110  30016  bnj1189  30165  noseponlem  30899  nodenselem4  30917  nodenselem5  30918  nofulllem5  30939  dfrecs2  31061  brub  31065  filnetlem4  31380  unblimceq0  31502  relowlpssretop  32212  matunitlindflem1  32399  poimirlem23  32426  poimirlem30  32433  poimirlem32  32435  poimir  32436  mblfinlem1  32440  fphpd  36222  fiphp3d  36225  rencldnfilem  36226  pellfundglb  36291  clsk3nimkb  37182  ndisj2  38067  eliin2f  38140  infrpge  38332  infxrbnd2  38350  limcrecl  38520  stoweidlem14  38731  stoweidlem34  38751  salexct  39052  vonioo  39397  vonicc  39400  n0snor2el  40143  umgr2edg1  40460  umgr2edgneu  40463  nfrgr2v  41464  4cycl2vnunb-av  41482  copisnmnd  41621  zrninitoringc  41885  pgrpgt2nabl  41963  islindeps  42058  islininds2  42089  ldepslinc  42114
  Copyright terms: Public domain W3C validator