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

Theorem rexnal 2978
 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 2977 . 2 (∀𝑥𝐴 𝜑 ↔ ¬ ∃𝑥𝐴 ¬ 𝜑)
21con2bii 346 1 (∃𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195  ∀wral 2896  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902 This theorem is referenced by:  rexnal2  3025  rexnal3  3026  2ralor  3088  elpwunsn  4171  n0snor2el  4304  uni0b  4399  iundif2  4523  weniso  6504  rexrnmpt2  6674  onnseq  7328  ixp0  7827  boxcutc  7837  isfinite2  8103  ordtypelem9  8314  ordtypelem10  8315  unbndrank  8588  tcrank  8630  infxpenlem  8719  kmlem3  8857  kmlem7  8861  kmlem8  8862  kmlem13  8867  cfeq0  8961  isf32lem2  9059  isf32lem5  9062  isf34lem4  9082  fin1a2lem7  9111  ac6n  9190  alephval2  9273  pwfseqlem3  9361  inttsk  9475  nqereu  9630  npomex  9697  prlem934  9734  arch  11166  qextlt  11908  qextle  11909  xralrple  11910  xrsupsslem  12009  xrinfmsslem  12010  supxrbnd1  12023  supxrbnd2  12024  supxrbnd  12030  fsuppmapnn0fiubex  12654  hashfun  13084  hashge2el2dif  13117  limsuplt  14058  fprodle  14566  alzdvds  14880  isprm5  15257  ncoprmlnprm  15274  pc2dvds  15421  vdwnn  15540  ramcl  15571  cshwshashlem1  15640  cshwshash  15649  isnsgrp  17111  isnmnd  17121  lt6abl  18119  mdetunilem8  20244  fctop  20618  cctop  20620  t0dist  20939  ist0-3  20959  pthaus  21251  txkgen  21265  xkohaus  21266  fbfinnfr  21455  isufil2  21522  hausflim  21595  fclscf  21639  bcth  22934  minveclem3b  23007  pmltpc  23026  volsup  23131  volsup2  23179  itg2seq  23315  itg2cn  23336  tdeglem4  23624  aaliou3lem9  23909  ftalem7  24605  dchrptlem3  24791  dchrsum2  24793  tglowdim1i  25196  tgdim01  25202  tglowdim2ln  25346  brbtwn2  25585  colinearalg  25590  axlowdimlem6  25627  axlowdimlem14  25635  usgra2edg1  25912  frgra2v  26526  4cycl2vnunb  26544  vdn0frgrav2  26550  vdgn0frgrav2  26551  nmounbi  27015  nmobndseqi  27018  minvecolem5  27121  xrnarchi  29069  isarchi2  29070  ordtconlem1  29298  lmdvg  29327  hasheuni  29474  voliune  29619  volfiniune  29620  ballotlemodife  29886  ballotlem4  29887  bnj1542  30181  bnj110  30182  bnj1189  30331  noseponlem  31065  nodenselem4  31083  nodenselem5  31084  nofulllem5  31105  dfrecs2  31227  brub  31231  filnetlem4  31546  unblimceq0  31668  relowlpssretop  32388  matunitlindflem1  32575  poimirlem23  32602  poimirlem30  32609  poimirlem32  32611  poimir  32612  mblfinlem1  32616  fphpd  36398  fiphp3d  36401  rencldnfilem  36402  pellfundglb  36467  clsk3nimkb  37358  ndisj2  38243  eliin2f  38316  infrpge  38508  infxrbnd2  38526  limcrecl  38696  stoweidlem14  38907  stoweidlem34  38927  salexct  39228  vonioo  39573  vonicc  39576  umgr2edg1  40438  umgr2edgneu  40441  nfrgr2v  41442  4cycl2vnunb-av  41460  copisnmnd  41599  zrninitoringc  41863  pgrpgt2nabl  41941  islindeps  42036  islininds2  42067  ldepslinc  42092
 Copyright terms: Public domain W3C validator