Theorem rexnal 3120

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3082  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3083  df-rex 3093

This theorem is used by:  r19.35  3126  r19.30  3135  rexnal2  3150  rexnal3  3151  raleq  3323  elpwunsn  4655  n0snor2el  4803  uni0b  4904  iundif2  5043  weniso  7365  rexrnmpo  7563  onnseq  8340  cofonr  8669  ixp0  8938  boxcutc  8948  isfinite2  9268  ordtypelem9  9498  ordtypelem10  9499  unbndrank  9824  tcrank  9866  infxpenlem  10016  kmlem3  10155  kmlem7  10159  kmlem8  10160  kmlem13  10165  cfeq0  10258  isf32lem2  10356  isf32lem5  10359  isf34lem4  10379  fin1a2lem7  10408  ac6n  10487  alephval2  10575  pwfseqlem3  10663  inttsk  10777  nqereu  10932  npomex  10999  prlem934  11036  arch  12519  qextlt  13247  qextle  13248  xralrple  13249  xrsupsslem  13351  xrinfmsslem  13352  supxrbnd1  13365  supxrbnd2  13366  supxrbnd  13372  fsuppmapnn0fiubex  14048  hashfun  14494  hashge2el2dif  14537  limsuplt  15556  fprodle  16076  alzdvds  16403  isprm5  16791  ncoprmlnprm  16812  pc2dvds  16964  vdwnn  17083  ramcl  17114  cshwshashlem1  17180  cshwshash  17189  isnsgrp  18810  isnmnd  18825  smndex1n0mnd  19005  lt6abl  19996  simpgnideld  20202  zrninitoringc  20812  ssdifidllem  21521  psdmul  22366  mdetunilem8  22813  fctop  23198  cctop  23200  t0dist  23519  ist0-3  23539  pthaus  23832  txkgen  23846  xkohaus  23847  fbfinnfr  24035  isufil2  24102  hausflim  24175  fclscf  24219  bcth  25525  minveclem3b  25624  pmltpc  25646  volsup  25752  volsup2  25801  itg2seq  25938  itg2cn  25959  tdeglem4  26254  aaliou3lem9  26550  ftalem7  27280  dchrptlem3  27467  dchrsum2  27469  noseponlem  27865  nolt02o  27896  noetasuplem4  27937  noetainflem4  27941  cofcutr  28154  tglowdim1i  28807  tglowdim2ln  28962  brbtwn2  29292  colinearalg  29297  axlowdimlem6  29334  axlowdimlem14  29342  umgr2edg1  29598  umgr2edgneu  29601  nfrgr2v  30660  4cycl2vnunb  30678  nmounbi  31165  nmobndseqi  31168  minvecolem5  31270  fprodex01  33206  xrnarchi  33535  isarchi2  33536  mxidlirred  33786  ssmxidllem  33787  fedgmullem2  34051  ordtconnlem1  34345  lmdvg  34374  hasheuni  34506  voliune  34651  volfiniune  34652  ballotlemodife  34920  ballotlem4  34921  reprdifc  35046  bnj1542  35277  bnj110  35278  bnj1189  35429  noinfepregs  35570  dfrecs2  36463  brub  36467  ltnadd  36731  naddle  36732  filnetlem4  36933  unblimceq0  37137  relowlpssretop  38051  nlpineqsn  38095  matunitlindflem1  38308  poimirlem23  38335  poimirlem30  38342  poimirlem32  38344  poimir  38345  mblfinlem1  38349  aks4d1p3  42886  aks4d1p8d2  42893  aks6d1c2p2  42927  aks6d1c5  42947  dffltz  43407  infdesc  43416  fphpd  43584  fiphp3d  43587  rencldnfilem  43588  pellfundglb  43653  onmaxnelsup  43991  onsupnmax  43996  ralopabb  44178  clsk3nimkb  44807  ndisj2  45812  eliin2f  45863  infrpge  46108  infxrbnd2  46125  supminfxr  46219  rexanuz2nf  46247  limcrecl  46386  limsupub  46459  limsuppnflem  46465  limsupre2lem  46479  stoweidlem14  46769  stoweidlem34  46789  salexct  47089  meaiuninc3v  47239  vonioo  47437  vonicc  47440  copisnmnd  48975  pgrpgt2nabl  49187  islindeps  49274  islininds2  49305  ldepslinc  49330  line2ylem  49572  line2xlem  49574  iineq0  49639  nelsubclem  49886  setc1onsubc  50421