Theorem rexnal 3089

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

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

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 3052  df-rex 3062

This theorem is referenced by:  r19.35  3095  r19.30  3104  rexnal2  3119  rexnal3  3120  raleq  3292  elpwunsn  4628  n0snor2el  4776  uni0b  4876  iundif2  5016  weniso  7309  rexrnmpo  7507  onnseq  8284  cofonr  8610  ixp0  8879  boxcutc  8889  isfinite2  9208  ordtypelem9  9441  ordtypelem10  9442  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  12434  qextlt  13155  qextle  13156  xralrple  13157  xrsupsslem  13259  xrinfmsslem  13260  supxrbnd1  13273  supxrbnd2  13274  supxrbnd  13280  fsuppmapnn0fiubex  13954  hashfun  14399  hashge2el2dif  14442  limsuplt  15441  fprodle  15961  alzdvds  16289  isprm5  16677  ncoprmlnprm  16698  pc2dvds  16850  vdwnn  16969  ramcl  17000  cshwshashlem1  17066  cshwshash  17075  isnsgrp  18691  isnmnd  18706  smndex1n0mnd  18883  lt6abl  19870  simpgnideld  20076  zrninitoringc  20653  psdmul  22132  mdetunilem8  22584  fctop  22969  cctop  22971  t0dist  23290  ist0-3  23310  pthaus  23603  txkgen  23617  xkohaus  23618  fbfinnfr  23806  isufil2  23873  hausflim  23946  fclscf  23990  bcth  25296  minveclem3b  25395  pmltpc  25417  volsup  25523  volsup2  25572  itg2seq  25709  itg2cn  25730  tdeglem4  26025  aaliou3lem9  26316  ftalem7  27042  dchrptlem3  27229  dchrsum2  27231  noseponlem  27628  nolt02o  27659  noetasuplem4  27700  noetainflem4  27704  cofcutr  27916  tglowdim1i  28569  tglowdim2ln  28719  brbtwn2  28974  colinearalg  28979  axlowdimlem6  29016  axlowdimlem14  29024  umgr2edg1  29280  umgr2edgneu  29283  nfrgr2v  30342  4cycl2vnunb  30360  nmounbi  30847  nmobndseqi  30850  minvecolem5  30952  fprodex01  32898  xrnarchi  33245  isarchi2  33246  ssdifidllem  33516  mxidlirred  33532  ssmxidllem  33533  fedgmullem2  33774  ordtconnlem1  34068  lmdvg  34097  hasheuni  34229  voliune  34373  volfiniune  34374  ballotlemodife  34642  ballotlem4  34643  reprdifc  34771  bnj1542  34999  bnj110  35000  bnj1189  35151  noinfepregs  35277  dfrecs2  36132  brub  36136  filnetlem4  36563  unblimceq0  36767  relowlpssretop  37680  nlpineqsn  37724  matunitlindflem1  37937  poimirlem23  37964  poimirlem30  37971  poimirlem32  37973  poimir  37974  mblfinlem1  37978  aks4d1p3  42517  aks4d1p8d2  42524  aks6d1c2p2  42558  aks6d1c5  42578  dffltz  43067  infdesc  43076  fphpd  43244  fiphp3d  43247  rencldnfilem  43248  pellfundglb  43313  onmaxnelsup  43651  onsupnmax  43656  ralopabb  43838  clsk3nimkb  44467  ndisj2  45482  eliin2f  45534  infrpge  45781  infxrbnd2  45798  supminfxr  45892  rexanuz2nf  45920  limcrecl  46059  limsupub  46132  limsuppnflem  46138  limsupre2lem  46152  stoweidlem14  46442  stoweidlem34  46462  salexct  46762  meaiuninc3v  46912  vonioo  47110  vonicc  47113  copisnmnd  48645  pgrpgt2nabl  48842  islindeps  48929  islininds2  48960  ldepslinc  48985  line2ylem  49227  line2xlem  49229  iineq0  49295  nelsubclem  49542  setc1onsubc  50077