Theorem rexnal 3092

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

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wral 3054  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3055  df-rex 3065

This theorem is referenced by:  r19.35  3098  r19.30  3107  rexnal2  3122  rexnal3  3123  raleq  3295  elpwunsn  4623  n0snor2el  4771  uni0b  4871  iundif2  5010  weniso  7305  rexrnmpo  7503  onnseq  8281  cofonr  8607  ixp0  8876  boxcutc  8886  isfinite2  9205  ordtypelem9  9438  ordtypelem10  9439  unbndrank  9764  tcrank  9806  infxpenlem  9933  kmlem3  10073  kmlem7  10077  kmlem8  10078  kmlem13  10083  cfeq0  10176  isf32lem2  10274  isf32lem5  10277  isf34lem4  10297  fin1a2lem7  10326  ac6n  10405  alephval2  10493  pwfseqlem3  10581  inttsk  10695  nqereu  10850  npomex  10917  prlem934  10954  arch  12432  qextlt  13153  qextle  13154  xralrple  13155  xrsupsslem  13257  xrinfmsslem  13258  supxrbnd1  13271  supxrbnd2  13272  supxrbnd  13278  fsuppmapnn0fiubex  13952  hashfun  14397  hashge2el2dif  14440  limsuplt  15439  fprodle  15959  alzdvds  16287  isprm5  16675  ncoprmlnprm  16696  pc2dvds  16848  vdwnn  16967  ramcl  16998  cshwshashlem1  17064  cshwshash  17073  isnsgrp  18689  isnmnd  18704  smndex1n0mnd  18881  lt6abl  19868  simpgnideld  20074  zrninitoringc  20655  psdmul  22161  mdetunilem8  22609  fctop  22994  cctop  22996  t0dist  23315  ist0-3  23335  pthaus  23628  txkgen  23642  xkohaus  23643  fbfinnfr  23831  isufil2  23898  hausflim  23971  fclscf  24015  bcth  25321  minveclem3b  25420  pmltpc  25442  volsup  25548  volsup2  25597  itg2seq  25734  itg2cn  25755  tdeglem4  26050  aaliou3lem9  26341  ftalem7  27067  dchrptlem3  27254  dchrsum2  27256  noseponlem  27653  nolt02o  27684  noetasuplem4  27725  noetainflem4  27729  cofcutr  27941  tglowdim1i  28594  tglowdim2ln  28744  brbtwn2  28999  colinearalg  29004  axlowdimlem6  29041  axlowdimlem14  29049  umgr2edg1  29305  umgr2edgneu  29308  nfrgr2v  30367  4cycl2vnunb  30385  nmounbi  30872  nmobndseqi  30875  minvecolem5  30977  fprodex01  32924  xrnarchi  33272  isarchi2  33273  ssdifidllem  33546  mxidlirred  33562  ssmxidllem  33563  fedgmullem2  33821  ordtconnlem1  34115  lmdvg  34144  hasheuni  34276  voliune  34420  volfiniune  34421  ballotlemodife  34689  ballotlem4  34690  reprdifc  34818  bnj1542  35046  bnj110  35047  bnj1189  35198  noinfepregs  35321  dfrecs2  36185  brub  36189  filnetlem4  36616  unblimceq0  36820  relowlpssretop  37733  nlpineqsn  37777  matunitlindflem1  37990  poimirlem23  38017  poimirlem30  38024  poimirlem32  38026  poimir  38027  mblfinlem1  38031  aks4d1p3  42570  aks4d1p8d2  42577  aks6d1c2p2  42611  aks6d1c5  42631  dffltz  43091  infdesc  43100  fphpd  43268  fiphp3d  43271  rencldnfilem  43272  pellfundglb  43337  onmaxnelsup  43675  onsupnmax  43680  ralopabb  43862  clsk3nimkb  44491  ndisj2  45506  eliin2f  45558  infrpge  45803  infxrbnd2  45820  supminfxr  45914  rexanuz2nf  45942  limcrecl  46081  limsupub  46154  limsuppnflem  46160  limsupre2lem  46174  stoweidlem14  46464  stoweidlem34  46484  salexct  46784  meaiuninc3v  46934  vonioo  47132  vonicc  47135  copisnmnd  48667  pgrpgt2nabl  48864  islindeps  48951  islininds2  48982  ldepslinc  49007  line2ylem  49249  line2xlem  49251  iineq0  49317  nelsubclem  49564  setc1onsubc  50099