Theorem rexnal 3118

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

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

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 3081  df-rex 3091

This theorem is used by:  r19.35  3124  r19.30  3133  rexnal2  3148  rexnal3  3149  raleq  3320  elpwunsn  4645  n0snor2el  4791  uni0b  4897  iundif2  5035  weniso  7390  rexrnmpo  7587  onnseq  8383  cofonr  8714  ixp0  8990  boxcutc  9000  isfinite2  9321  ordtypelem9  9550  ordtypelem10  9551  unbndrank  9885  tcrank  9931  infxpenlem  10122  kmlem3  10261  kmlem7  10265  kmlem8  10266  kmlem13  10271  cfeq0  10364  isf32lem2  10462  isf32lem5  10465  isf34lem4  10485  fin1a2lem7  10514  ac6n  10593  alephval2  10687  pwfseqlem3  10775  inttsk  10889  nqereu  11044  npomex  11111  prlem934  11148  arch  12633  qextlt  13363  qextle  13364  xralrple  13365  xrsupsslem  13467  xrinfmsslem  13468  supxrbnd1  13481  supxrbnd2  13482  supxrbnd  13488  fsuppmapnn0fiubex  14165  hashfun  14612  hashge2el2dif  14655  limsuplt  15678  fprodle  16195  alzdvds  16522  isprm5  16915  ncoprmlnprm  16936  pc2dvds  17089  vdwnn  17208  ramcl  17239  cshwshashlem1  17305  cshwshash  17314  isnsgrp  18944  isnmnd  18959  smndex1n0mnd  19143  lt6abl  20142  simpgnideld  20348  zrninitoringc  20961  ssdifidllem  21673  psdmul  22520  mdetunilem8  22967  matunitlindflem1  23027  fctop  23355  cctop  23357  t0dist  23676  ist0-3  23696  pthaus  23990  txkgen  24004  xkohaus  24005  fbfinnfr  24193  isufil2  24260  hausflim  24333  fclscf  24377  bcth  25683  minveclem3b  25782  pmltpc  25804  volsup  25910  volsup2  25959  itg2seq  26096  itg2cn  26117  tdeglem4  26411  rnplynfin  26663  plyconz  26664  aaliou3lem9  26710  ftalem7  27439  dchrptlem3  27626  dchrsum2  27628  infdesc  28000  noseponlem  28054  nolt02o  28085  noetasuplem4  28126  noetainflem4  28130  cofcutr  28343  tglowdim1i  28997  tglowdim2ln  29153  brbtwn2  29516  colinearalg  29521  axlowdimlem6  29558  axlowdimlem14  29566  umgr2edg1  29825  umgr2edgneu  29828  nfrgr2v  30906  4cycl2vnunb  30924  nmounbi  31411  nmobndseqi  31414  minvecolem5  31516  fprodex01  33489  xrnarchi  33821  isarchi2  33822  mxidlirred  34081  ssmxidllem  34082  fedgmullem2  34345  ordtconnlem1  34639  lmdvg  34668  hasheuni  34800  voliune  34945  volfiniune  34946  ballotlemodife  35213  ballotlem4  35214  reprdifc  35339  bnj1542  35570  bnj110  35571  bnj1189  35722  noinfepregs  35914  dfrecs2  36905  brub  36909  ltnadd  37158  naddle  37159  filnetlem4  37360  unblimceq0  37564  relowlpssretop  38492  nlpineqsn  38536  poimirlem23  38766  poimirlem30  38773  poimirlem32  38775  poimir  38776  mblfinlem1  38780  aks4d1p3  43331  aks4d1p8d2  43338  aks6d1c2p2  43372  aks6d1c5  43392  dffltz  43874  fphpd  44027  fiphp3d  44030  rencldnfilem  44031  pellfundglb  44096  onmaxnelsup  44428  onsupnmax  44433  ralopabb  44615  clsk3nimkb  45243  ndisj2  46284  eliin2f  46334  infrpge  46578  infxrbnd2  46595  supminfxr  46689  rexanuz2nf  46717  limcrecl  46856  limsupub  46929  limsuppnflem  46935  limsupre2lem  46949  stoweidlem14  47239  stoweidlem34  47259  salexct  47559  meaiuninc3v  47709  vonioo  47907  vonicc  47910  copisnmnd  49481  pgrpgt2nabl  49693  islindeps  49780  islininds2  49811  ldepslinc  49836  line2ylem  50078  line2xlem  50080  iineq0  50146  nelsubclem  50396  setc1onsubc  50955