Theorem rexnal 3090

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3052  ∃wrex 3062

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 3053  df-rex 3063

This theorem is referenced by:  r19.35  3096  r19.30  3105  rexnal2  3120  rexnal3  3121  raleq  3293  elpwunsn  4629  n0snor2el  4777  uni0b  4877  iundif2  5017  weniso  7302  rexrnmpo  7500  onnseq  8277  cofonr  8603  ixp0  8872  boxcutc  8882  isfinite2  9201  ordtypelem9  9434  ordtypelem10  9435  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  10486  pwfseqlem3  10574  inttsk  10688  nqereu  10843  npomex  10910  prlem934  10947  arch  12425  qextlt  13146  qextle  13147  xralrple  13148  xrsupsslem  13250  xrinfmsslem  13251  supxrbnd1  13264  supxrbnd2  13265  supxrbnd  13271  fsuppmapnn0fiubex  13945  hashfun  14390  hashge2el2dif  14433  limsuplt  15432  fprodle  15952  alzdvds  16280  isprm5  16668  ncoprmlnprm  16689  pc2dvds  16841  vdwnn  16960  ramcl  16991  cshwshashlem1  17057  cshwshash  17066  isnsgrp  18682  isnmnd  18697  smndex1n0mnd  18874  lt6abl  19861  simpgnideld  20067  zrninitoringc  20644  psdmul  22142  mdetunilem8  22594  fctop  22979  cctop  22981  t0dist  23300  ist0-3  23320  pthaus  23613  txkgen  23627  xkohaus  23628  fbfinnfr  23816  isufil2  23883  hausflim  23956  fclscf  24000  bcth  25306  minveclem3b  25405  pmltpc  25427  volsup  25533  volsup2  25582  itg2seq  25719  itg2cn  25740  tdeglem4  26035  aaliou3lem9  26327  ftalem7  27056  dchrptlem3  27243  dchrsum2  27245  noseponlem  27642  nolt02o  27673  noetasuplem4  27714  noetainflem4  27718  cofcutr  27930  tglowdim1i  28583  tglowdim2ln  28733  brbtwn2  28988  colinearalg  28993  axlowdimlem6  29030  axlowdimlem14  29038  umgr2edg1  29294  umgr2edgneu  29297  nfrgr2v  30357  4cycl2vnunb  30375  nmounbi  30862  nmobndseqi  30865  minvecolem5  30967  fprodex01  32913  xrnarchi  33260  isarchi2  33261  ssdifidllem  33531  mxidlirred  33547  ssmxidllem  33548  fedgmullem2  33790  ordtconnlem1  34084  lmdvg  34113  hasheuni  34245  voliune  34389  volfiniune  34390  ballotlemodife  34658  ballotlem4  34659  reprdifc  34787  bnj1542  35015  bnj110  35016  bnj1189  35167  noinfepregs  35293  dfrecs2  36148  brub  36152  filnetlem4  36579  unblimceq0  36783  relowlpssretop  37694  nlpineqsn  37738  matunitlindflem1  37951  poimirlem23  37978  poimirlem30  37985  poimirlem32  37987  poimir  37988  mblfinlem1  37992  aks4d1p3  42531  aks4d1p8d2  42538  aks6d1c2p2  42572  aks6d1c5  42592  dffltz  43081  infdesc  43090  fphpd  43262  fiphp3d  43265  rencldnfilem  43266  pellfundglb  43331  onmaxnelsup  43669  onsupnmax  43674  ralopabb  43856  clsk3nimkb  44485  ndisj2  45500  eliin2f  45552  infrpge  45799  infxrbnd2  45816  supminfxr  45910  rexanuz2nf  45938  limcrecl  46077  limsupub  46150  limsuppnflem  46156  limsupre2lem  46170  stoweidlem14  46460  stoweidlem34  46480  salexct  46780  meaiuninc3v  46930  vonioo  47128  vonicc  47131  copisnmnd  48657  pgrpgt2nabl  48854  islindeps  48941  islininds2  48972  ldepslinc  48997  line2ylem  49239  line2xlem  49241  iineq0  49307  nelsubclem  49554  setc1onsubc  50089