Theorem rexnal 3106

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3067  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  r19.35  3114  r19.35OLD  3115  r19.30  3126  rexnal2  3141  rexnal3  3142  2ralorOLD  3238  raleq  3331  elpwunsn  4707  n0snor2el  4858  uni0b  4957  iundif2  5097  weniso  7390  rexrnmpo  7590  onnseq  8400  cofonr  8730  ixp0  8989  boxcutc  8999  isfinite2  9362  ordtypelem9  9595  ordtypelem10  9596  unbndrank  9911  tcrank  9953  infxpenlem  10082  kmlem3  10222  kmlem7  10226  kmlem8  10227  kmlem13  10232  cfeq0  10325  isf32lem2  10423  isf32lem5  10426  isf34lem4  10446  fin1a2lem7  10475  ac6n  10554  alephval2  10641  pwfseqlem3  10729  inttsk  10843  nqereu  10998  npomex  11065  prlem934  11102  arch  12550  qextlt  13265  qextle  13266  xralrple  13267  xrsupsslem  13369  xrinfmsslem  13370  supxrbnd1  13383  supxrbnd2  13384  supxrbnd  13390  fsuppmapnn0fiubex  14043  hashfun  14486  hashge2el2dif  14529  limsuplt  15525  fprodle  16044  alzdvds  16368  isprm5  16754  ncoprmlnprm  16775  pc2dvds  16926  vdwnn  17045  ramcl  17076  cshwshashlem1  17143  cshwshash  17152  isnsgrp  18761  isnmnd  18776  smndex1n0mnd  18947  lt6abl  19937  simpgnideld  20143  zrninitoringc  20698  psdmul  22193  mdetunilem8  22646  fctop  23032  cctop  23034  t0dist  23354  ist0-3  23374  pthaus  23667  txkgen  23681  xkohaus  23682  fbfinnfr  23870  isufil2  23937  hausflim  24010  fclscf  24054  bcth  25382  minveclem3b  25481  pmltpc  25504  volsup  25610  volsup2  25659  itg2seq  25797  itg2cn  25818  tdeglem4  26119  aaliou3lem9  26410  ftalem7  27140  dchrptlem3  27328  dchrsum2  27330  noseponlem  27727  nolt02o  27758  noetasuplem4  27799  noetainflem4  27803  cofcutr  27976  tglowdim1i  28527  tglowdim2ln  28677  brbtwn2  28938  colinearalg  28943  axlowdimlem6  28980  axlowdimlem14  28988  umgr2edg1  29246  umgr2edgneu  29249  nfrgr2v  30304  4cycl2vnunb  30322  nmounbi  30808  nmobndseqi  30811  minvecolem5  30913  fprodex01  32829  xrnarchi  33164  isarchi2  33165  ssdifidllem  33449  mxidlirred  33465  ssmxidllem  33466  fedgmullem2  33643  ordtconnlem1  33870  lmdvg  33899  hasheuni  34049  voliune  34193  volfiniune  34194  ballotlemodife  34462  ballotlem4  34463  reprdifc  34604  bnj1542  34833  bnj110  34834  bnj1189  34985  dfrecs2  35914  brub  35918  filnetlem4  36347  unblimceq0  36473  relowlpssretop  37330  nlpineqsn  37374  matunitlindflem1  37576  poimirlem23  37603  poimirlem30  37610  poimirlem32  37612  poimir  37613  mblfinlem1  37617  aks4d1p3  42035  aks4d1p8d2  42042  aks6d1c2p2  42076  aks6d1c5  42096  dffltz  42589  infdesc  42598  fphpd  42772  fiphp3d  42775  rencldnfilem  42776  pellfundglb  42841  onmaxnelsup  43184  onsupnmax  43189  ralopabb  43373  clsk3nimkb  44002  ndisj2  44953  eliin2f  45006  infrpge  45266  infxrbnd2  45284  supminfxr  45379  rexanuz2nf  45408  limcrecl  45550  limsupub  45625  limsuppnflem  45631  limsupre2lem  45645  stoweidlem14  45935  stoweidlem34  45955  salexct  46255  meaiuninc3v  46405  vonioo  46603  vonicc  46606  tworepnotupword  46805  copisnmnd  47892  pgrpgt2nabl  48091  islindeps  48182  islininds2  48213  ldepslinc  48238  line2ylem  48485  line2xlem  48487