Theorem rexnal 3093

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 3092	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
2	1	con2bii 359	1 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wral 3055  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-ral 3056  df-rex 3066

This theorem is referenced by:  r19.35  3099  r19.30  3108  rexnal2  3123  rexnal3  3124  raleq  3296  elpwunsn  4619  n0snor2el  4767  uni0b  4867  iundif2  5006  weniso  7302  rexrnmpo  7500  onnseq  8278  cofonr  8604  ixp0  8873  boxcutc  8883  isfinite2  9202  ordtypelem9  9435  ordtypelem10  9436  unbndrank  9761  tcrank  9803  infxpenlem  9930  kmlem3  10070  kmlem7  10074  kmlem8  10075  kmlem13  10080  cfeq0  10173  isf32lem2  10271  isf32lem5  10274  isf34lem4  10294  fin1a2lem7  10323  ac6n  10402  alephval2  10490  pwfseqlem3  10578  inttsk  10692  nqereu  10847  npomex  10914  prlem934  10951  arch  12429  qextlt  13150  qextle  13151  xralrple  13152  xrsupsslem  13254  xrinfmsslem  13255  supxrbnd1  13268  supxrbnd2  13269  supxrbnd  13275  fsuppmapnn0fiubex  13949  hashfun  14394  hashge2el2dif  14437  limsuplt  15436  fprodle  15956  alzdvds  16284  isprm5  16672  ncoprmlnprm  16693  pc2dvds  16845  vdwnn  16964  ramcl  16995  cshwshashlem1  17061  cshwshash  17070  isnsgrp  18686  isnmnd  18701  smndex1n0mnd  18878  lt6abl  19865  simpgnideld  20071  zrninitoringc  20652  psdmul  22158  mdetunilem8  22606  fctop  22991  cctop  22993  t0dist  23312  ist0-3  23332  pthaus  23625  txkgen  23639  xkohaus  23640  fbfinnfr  23828  isufil2  23895  hausflim  23968  fclscf  24012  bcth  25318  minveclem3b  25417  pmltpc  25439  volsup  25545  volsup2  25594  itg2seq  25731  itg2cn  25752  tdeglem4  26047  aaliou3lem9  26338  ftalem7  27064  dchrptlem3  27251  dchrsum2  27253  noseponlem  27650  nolt02o  27681  noetasuplem4  27722  noetainflem4  27726  cofcutr  27938  tglowdim1i  28591  tglowdim2ln  28741  brbtwn2  28996  colinearalg  29001  axlowdimlem6  29038  axlowdimlem14  29046  umgr2edg1  29302  umgr2edgneu  29305  nfrgr2v  30364  4cycl2vnunb  30382  nmounbi  30869  nmobndseqi  30872  minvecolem5  30974  fprodex01  32921  xrnarchi  33269  isarchi2  33270  ssdifidllem  33543  mxidlirred  33559  ssmxidllem  33560  fedgmullem2  33826  ordtconnlem1  34120  lmdvg  34149  hasheuni  34281  voliune  34425  volfiniune  34426  ballotlemodife  34694  ballotlem4  34695  reprdifc  34823  bnj1542  35054  bnj110  35055  bnj1189  35206  noinfepregs  35329  dfrecs2  36193  brub  36197  filnetlem4  36624  unblimceq0  36828  relowlpssretop  37741  nlpineqsn  37785  matunitlindflem1  37998  poimirlem23  38025  poimirlem30  38032  poimirlem32  38034  poimir  38035  mblfinlem1  38039  aks4d1p3  42578  aks4d1p8d2  42585  aks6d1c2p2  42619  aks6d1c5  42639  dffltz  43099  infdesc  43108  fphpd  43276  fiphp3d  43279  rencldnfilem  43280  pellfundglb  43345  onmaxnelsup  43683  onsupnmax  43688  ralopabb  43870  clsk3nimkb  44499  ndisj2  45514  eliin2f  45565  infrpge  45810  infxrbnd2  45827  supminfxr  45921  rexanuz2nf  45949  limcrecl  46088  limsupub  46161  limsuppnflem  46167  limsupre2lem  46181  stoweidlem14  46471  stoweidlem34  46491  salexct  46791  meaiuninc3v  46941  vonioo  47139  vonicc  47142  copisnmnd  48674  pgrpgt2nabl  48871  islindeps  48958  islininds2  48989  ldepslinc  49014  line2ylem  49256  line2xlem  49258  iineq0  49324  nelsubclem  49571  setc1onsubc  50106