Theorem rexnal 3090

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3052  ∃wrex 3062

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 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  r19.35  3096  r19.30  3105  rexnal2  3120  rexnal3  3121  raleq  3295  elpwunsn  4643  n0snor2el  4791  uni0b  4891  iundif2  5031  weniso  7310  rexrnmpo  7508  onnseq  8286  cofonr  8612  ixp0  8881  boxcutc  8891  isfinite2  9210  ordtypelem9  9443  ordtypelem10  9444  unbndrank  9766  tcrank  9808  infxpenlem  9935  kmlem3  10075  kmlem7  10079  kmlem8  10080  kmlem13  10085  cfeq0  10178  isf32lem2  10276  isf32lem5  10279  isf34lem4  10299  fin1a2lem7  10328  ac6n  10407  alephval2  10495  pwfseqlem3  10583  inttsk  10697  nqereu  10852  npomex  10919  prlem934  10956  arch  12410  qextlt  13130  qextle  13131  xralrple  13132  xrsupsslem  13234  xrinfmsslem  13235  supxrbnd1  13248  supxrbnd2  13249  supxrbnd  13255  fsuppmapnn0fiubex  13927  hashfun  14372  hashge2el2dif  14415  limsuplt  15414  fprodle  15931  alzdvds  16259  isprm5  16646  ncoprmlnprm  16667  pc2dvds  16819  vdwnn  16938  ramcl  16969  cshwshashlem1  17035  cshwshash  17044  isnsgrp  18660  isnmnd  18675  smndex1n0mnd  18849  lt6abl  19836  simpgnideld  20042  zrninitoringc  20621  psdmul  22121  mdetunilem8  22575  fctop  22960  cctop  22962  t0dist  23281  ist0-3  23301  pthaus  23594  txkgen  23608  xkohaus  23609  fbfinnfr  23797  isufil2  23864  hausflim  23937  fclscf  23981  bcth  25297  minveclem3b  25396  pmltpc  25419  volsup  25525  volsup2  25574  itg2seq  25711  itg2cn  25732  tdeglem4  26033  aaliou3lem9  26326  ftalem7  27057  dchrptlem3  27245  dchrsum2  27247  noseponlem  27644  nolt02o  27675  noetasuplem4  27716  noetainflem4  27720  cofcutr  27932  tglowdim1i  28585  tglowdim2ln  28735  brbtwn2  28990  colinearalg  28995  axlowdimlem6  29032  axlowdimlem14  29040  umgr2edg1  29296  umgr2edgneu  29299  nfrgr2v  30359  4cycl2vnunb  30377  nmounbi  30863  nmobndseqi  30866  minvecolem5  30968  fprodex01  32916  xrnarchi  33277  isarchi2  33278  ssdifidllem  33548  mxidlirred  33564  ssmxidllem  33565  fedgmullem2  33807  ordtconnlem1  34101  lmdvg  34130  hasheuni  34262  voliune  34406  volfiniune  34407  ballotlemodife  34675  ballotlem4  34676  reprdifc  34804  bnj1542  35032  bnj110  35033  bnj1189  35184  noinfepregs  35308  dfrecs2  36163  brub  36167  filnetlem4  36594  unblimceq0  36726  relowlpssretop  37613  nlpineqsn  37657  matunitlindflem1  37861  poimirlem23  37888  poimirlem30  37895  poimirlem32  37897  poimir  37898  mblfinlem1  37902  aks4d1p3  42442  aks4d1p8d2  42449  aks6d1c2p2  42483  aks6d1c5  42503  dffltz  42986  infdesc  42995  fphpd  43167  fiphp3d  43170  rencldnfilem  43171  pellfundglb  43236  onmaxnelsup  43574  onsupnmax  43579  ralopabb  43761  clsk3nimkb  44390  ndisj2  45405  eliin2f  45457  infrpge  45704  infxrbnd2  45721  supminfxr  45816  rexanuz2nf  45844  limcrecl  45983  limsupub  46056  limsuppnflem  46062  limsupre2lem  46076  stoweidlem14  46366  stoweidlem34  46386  salexct  46686  meaiuninc3v  46836  vonioo  47034  vonicc  47037  copisnmnd  48523  pgrpgt2nabl  48720  islindeps  48807  islininds2  48838  ldepslinc  48863  line2ylem  49105  line2xlem  49107  iineq0  49173  nelsubclem  49420  setc1onsubc  49955