Theorem rexnal 3098

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

Step	Hyp	Ref	Expression
1		dfral2 3097	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
2	1	con2bii 357	1 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3059  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069

This theorem is referenced by:  r19.35  3106  r19.35OLD  3107  r19.30  3118  rexnal2  3133  rexnal3  3134  2ralorOLD  3230  raleq  3321  elpwunsn  4689  n0snor2el  4838  uni0b  4938  iundif2  5079  weniso  7374  rexrnmpo  7573  onnseq  8383  cofonr  8711  ixp0  8970  boxcutc  8980  isfinite2  9332  ordtypelem9  9564  ordtypelem10  9565  unbndrank  9880  tcrank  9922  infxpenlem  10051  kmlem3  10191  kmlem7  10195  kmlem8  10196  kmlem13  10201  cfeq0  10294  isf32lem2  10392  isf32lem5  10395  isf34lem4  10415  fin1a2lem7  10444  ac6n  10523  alephval2  10610  pwfseqlem3  10698  inttsk  10812  nqereu  10967  npomex  11034  prlem934  11071  arch  12521  qextlt  13242  qextle  13243  xralrple  13244  xrsupsslem  13346  xrinfmsslem  13347  supxrbnd1  13360  supxrbnd2  13361  supxrbnd  13367  fsuppmapnn0fiubex  14030  hashfun  14473  hashge2el2dif  14516  limsuplt  15512  fprodle  16029  alzdvds  16354  isprm5  16741  ncoprmlnprm  16762  pc2dvds  16913  vdwnn  17032  ramcl  17063  cshwshashlem1  17130  cshwshash  17139  isnsgrp  18749  isnmnd  18764  smndex1n0mnd  18938  lt6abl  19928  simpgnideld  20134  zrninitoringc  20693  psdmul  22188  mdetunilem8  22641  fctop  23027  cctop  23029  t0dist  23349  ist0-3  23369  pthaus  23662  txkgen  23676  xkohaus  23677  fbfinnfr  23865  isufil2  23932  hausflim  24005  fclscf  24049  bcth  25377  minveclem3b  25476  pmltpc  25499  volsup  25605  volsup2  25654  itg2seq  25792  itg2cn  25813  tdeglem4  26114  aaliou3lem9  26407  ftalem7  27137  dchrptlem3  27325  dchrsum2  27327  noseponlem  27724  nolt02o  27755  noetasuplem4  27796  noetainflem4  27800  cofcutr  27973  tglowdim1i  28524  tglowdim2ln  28674  brbtwn2  28935  colinearalg  28940  axlowdimlem6  28977  axlowdimlem14  28985  umgr2edg1  29243  umgr2edgneu  29246  nfrgr2v  30301  4cycl2vnunb  30319  nmounbi  30805  nmobndseqi  30808  minvecolem5  30910  fprodex01  32832  xrnarchi  33174  isarchi2  33175  ssdifidllem  33464  mxidlirred  33480  ssmxidllem  33481  fedgmullem2  33658  ordtconnlem1  33885  lmdvg  33914  hasheuni  34066  voliune  34210  volfiniune  34211  ballotlemodife  34479  ballotlem4  34480  reprdifc  34621  bnj1542  34850  bnj110  34851  bnj1189  35002  dfrecs2  35932  brub  35936  filnetlem4  36364  unblimceq0  36490  relowlpssretop  37347  nlpineqsn  37391  matunitlindflem1  37603  poimirlem23  37630  poimirlem30  37637  poimirlem32  37639  poimir  37640  mblfinlem1  37644  aks4d1p3  42060  aks4d1p8d2  42067  aks6d1c2p2  42101  aks6d1c5  42121  dffltz  42621  infdesc  42630  fphpd  42804  fiphp3d  42807  rencldnfilem  42808  pellfundglb  42873  onmaxnelsup  43212  onsupnmax  43217  ralopabb  43401  clsk3nimkb  44030  ndisj2  44991  eliin2f  45044  infrpge  45301  infxrbnd2  45319  supminfxr  45414  rexanuz2nf  45443  limcrecl  45585  limsupub  45660  limsuppnflem  45666  limsupre2lem  45680  stoweidlem14  45970  stoweidlem34  45990  salexct  46290  meaiuninc3v  46440  vonioo  46638  vonicc  46641  tworepnotupword  46840  copisnmnd  48013  pgrpgt2nabl  48211  islindeps  48299  islininds2  48330  ldepslinc  48355  line2ylem  48601  line2xlem  48603