Theorem rexnal 3088

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3051  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052  df-rex 3061

This theorem is referenced by:  r19.35  3094  r19.30  3103  rexnal2  3118  rexnal3  3119  raleq  3293  elpwunsn  4641  n0snor2el  4789  uni0b  4889  iundif2  5029  weniso  7300  rexrnmpo  7498  onnseq  8276  cofonr  8602  ixp0  8869  boxcutc  8879  isfinite2  9198  ordtypelem9  9431  ordtypelem10  9432  unbndrank  9754  tcrank  9796  infxpenlem  9923  kmlem3  10063  kmlem7  10067  kmlem8  10068  kmlem13  10073  cfeq0  10166  isf32lem2  10264  isf32lem5  10267  isf34lem4  10287  fin1a2lem7  10316  ac6n  10395  alephval2  10483  pwfseqlem3  10571  inttsk  10685  nqereu  10840  npomex  10907  prlem934  10944  arch  12398  qextlt  13118  qextle  13119  xralrple  13120  xrsupsslem  13222  xrinfmsslem  13223  supxrbnd1  13236  supxrbnd2  13237  supxrbnd  13243  fsuppmapnn0fiubex  13915  hashfun  14360  hashge2el2dif  14403  limsuplt  15402  fprodle  15919  alzdvds  16247  isprm5  16634  ncoprmlnprm  16655  pc2dvds  16807  vdwnn  16926  ramcl  16957  cshwshashlem1  17023  cshwshash  17032  isnsgrp  18648  isnmnd  18663  smndex1n0mnd  18837  lt6abl  19824  simpgnideld  20030  zrninitoringc  20609  psdmul  22109  mdetunilem8  22563  fctop  22948  cctop  22950  t0dist  23269  ist0-3  23289  pthaus  23582  txkgen  23596  xkohaus  23597  fbfinnfr  23785  isufil2  23852  hausflim  23925  fclscf  23969  bcth  25285  minveclem3b  25384  pmltpc  25407  volsup  25513  volsup2  25562  itg2seq  25699  itg2cn  25720  tdeglem4  26021  aaliou3lem9  26314  ftalem7  27045  dchrptlem3  27233  dchrsum2  27235  noseponlem  27632  nolt02o  27663  noetasuplem4  27704  noetainflem4  27708  cofcutr  27920  tglowdim1i  28573  tglowdim2ln  28723  brbtwn2  28978  colinearalg  28983  axlowdimlem6  29020  axlowdimlem14  29028  umgr2edg1  29284  umgr2edgneu  29287  nfrgr2v  30347  4cycl2vnunb  30365  nmounbi  30851  nmobndseqi  30854  minvecolem5  30956  fprodex01  32906  xrnarchi  33266  isarchi2  33267  ssdifidllem  33537  mxidlirred  33553  ssmxidllem  33554  fedgmullem2  33787  ordtconnlem1  34081  lmdvg  34110  hasheuni  34242  voliune  34386  volfiniune  34387  ballotlemodife  34655  ballotlem4  34656  reprdifc  34784  bnj1542  35013  bnj110  35014  bnj1189  35165  noinfepregs  35289  dfrecs2  36144  brub  36148  filnetlem4  36575  unblimceq0  36707  relowlpssretop  37565  nlpineqsn  37609  matunitlindflem1  37813  poimirlem23  37840  poimirlem30  37847  poimirlem32  37849  poimir  37850  mblfinlem1  37854  aks4d1p3  42328  aks4d1p8d2  42335  aks6d1c2p2  42369  aks6d1c5  42389  dffltz  42873  infdesc  42882  fphpd  43054  fiphp3d  43057  rencldnfilem  43058  pellfundglb  43123  onmaxnelsup  43461  onsupnmax  43466  ralopabb  43648  clsk3nimkb  44277  ndisj2  45292  eliin2f  45344  infrpge  45592  infxrbnd2  45609  supminfxr  45704  rexanuz2nf  45732  limcrecl  45871  limsupub  45944  limsuppnflem  45950  limsupre2lem  45964  stoweidlem14  46254  stoweidlem34  46274  salexct  46574  meaiuninc3v  46724  vonioo  46922  vonicc  46925  copisnmnd  48411  pgrpgt2nabl  48608  islindeps  48695  islininds2  48726  ldepslinc  48751  line2ylem  48993  line2xlem  48995  iineq0  49061  nelsubclem  49308  setc1onsubc  49843