Theorem rexnal 3081

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3044  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  r19.35  3087  r19.30  3096  rexnal2  3111  rexnal3  3112  raleq  3287  elpwunsn  4638  n0snor2el  4787  uni0b  4887  iundif2  5026  weniso  7295  rexrnmpo  7493  onnseq  8274  cofonr  8599  ixp0  8865  boxcutc  8875  isfinite2  9203  ordtypelem9  9437  ordtypelem10  9438  unbndrank  9757  tcrank  9799  infxpenlem  9926  kmlem3  10066  kmlem7  10070  kmlem8  10071  kmlem13  10076  cfeq0  10169  isf32lem2  10267  isf32lem5  10270  isf34lem4  10290  fin1a2lem7  10319  ac6n  10398  alephval2  10485  pwfseqlem3  10573  inttsk  10687  nqereu  10842  npomex  10909  prlem934  10946  arch  12399  qextlt  13123  qextle  13124  xralrple  13125  xrsupsslem  13227  xrinfmsslem  13228  supxrbnd1  13241  supxrbnd2  13242  supxrbnd  13248  fsuppmapnn0fiubex  13917  hashfun  14362  hashge2el2dif  14405  limsuplt  15404  fprodle  15921  alzdvds  16249  isprm5  16636  ncoprmlnprm  16657  pc2dvds  16809  vdwnn  16928  ramcl  16959  cshwshashlem1  17025  cshwshash  17034  isnsgrp  18615  isnmnd  18630  smndex1n0mnd  18804  lt6abl  19792  simpgnideld  19998  zrninitoringc  20579  psdmul  22069  mdetunilem8  22522  fctop  22907  cctop  22909  t0dist  23228  ist0-3  23248  pthaus  23541  txkgen  23555  xkohaus  23556  fbfinnfr  23744  isufil2  23811  hausflim  23884  fclscf  23928  bcth  25245  minveclem3b  25344  pmltpc  25367  volsup  25473  volsup2  25522  itg2seq  25659  itg2cn  25680  tdeglem4  25981  aaliou3lem9  26274  ftalem7  27005  dchrptlem3  27193  dchrsum2  27195  noseponlem  27592  nolt02o  27623  noetasuplem4  27664  noetainflem4  27668  cofcutr  27855  tglowdim1i  28464  tglowdim2ln  28614  brbtwn2  28868  colinearalg  28873  axlowdimlem6  28910  axlowdimlem14  28918  umgr2edg1  29174  umgr2edgneu  29177  nfrgr2v  30234  4cycl2vnunb  30252  nmounbi  30738  nmobndseqi  30741  minvecolem5  30843  fprodex01  32783  xrnarchi  33136  isarchi2  33137  ssdifidllem  33403  mxidlirred  33419  ssmxidllem  33420  fedgmullem2  33602  ordtconnlem1  33890  lmdvg  33919  hasheuni  34051  voliune  34195  volfiniune  34196  ballotlemodife  34465  ballotlem4  34466  reprdifc  34594  bnj1542  34823  bnj110  34824  bnj1189  34975  dfrecs2  35923  brub  35927  filnetlem4  36354  unblimceq0  36480  relowlpssretop  37337  nlpineqsn  37381  matunitlindflem1  37595  poimirlem23  37622  poimirlem30  37629  poimirlem32  37631  poimir  37632  mblfinlem1  37636  aks4d1p3  42051  aks4d1p8d2  42058  aks6d1c2p2  42092  aks6d1c5  42112  dffltz  42607  infdesc  42616  fphpd  42789  fiphp3d  42792  rencldnfilem  42793  pellfundglb  42858  onmaxnelsup  43196  onsupnmax  43201  ralopabb  43384  clsk3nimkb  44013  ndisj2  45029  eliin2f  45082  infrpge  45331  infxrbnd2  45349  supminfxr  45444  rexanuz2nf  45472  limcrecl  45611  limsupub  45686  limsuppnflem  45692  limsupre2lem  45706  stoweidlem14  45996  stoweidlem34  46016  salexct  46316  meaiuninc3v  46466  vonioo  46664  vonicc  46667  tworepnotupword  46868  copisnmnd  48154  pgrpgt2nabl  48351  islindeps  48439  islininds2  48470  ldepslinc  48495  line2ylem  48737  line2xlem  48739  iineq0  48805  nelsubclem  49053  setc1onsubc  49588