Theorem rexnal 3165

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3063  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexnal2  3186  rexnal3  3187  r19.30  3265  r19.35  3268  2ralorOLD  3295  elpwunsn  4616  n0snor2el  4761  uni0b  4864  iundif2  4999  weniso  7205  rexrnmpo  7391  onnseq  8146  ixp0  8677  boxcutc  8687  isfinite2  9002  ordtypelem9  9215  ordtypelem10  9216  unbndrank  9531  tcrank  9573  infxpenlem  9700  kmlem3  9839  kmlem7  9843  kmlem8  9844  kmlem13  9849  cfeq0  9943  isf32lem2  10041  isf32lem5  10044  isf34lem4  10064  fin1a2lem7  10093  ac6n  10172  alephval2  10259  pwfseqlem3  10347  inttsk  10461  nqereu  10616  npomex  10683  prlem934  10720  arch  12160  qextlt  12866  qextle  12867  xralrple  12868  xrsupsslem  12970  xrinfmsslem  12971  supxrbnd1  12984  supxrbnd2  12985  supxrbnd  12991  fsuppmapnn0fiubex  13640  hashfun  14080  hashge2el2dif  14122  limsuplt  15116  fprodle  15634  alzdvds  15957  isprm5  16340  ncoprmlnprm  16360  pc2dvds  16508  vdwnn  16627  ramcl  16658  cshwshashlem1  16725  cshwshash  16734  isnsgrp  18294  isnmnd  18304  smndex1n0mnd  18466  lt6abl  19411  simpgnideld  19617  mdetunilem8  21676  fctop  22062  cctop  22064  t0dist  22384  ist0-3  22404  pthaus  22697  txkgen  22711  xkohaus  22712  fbfinnfr  22900  isufil2  22967  hausflim  23040  fclscf  23084  bcth  24398  minveclem3b  24497  pmltpc  24519  volsup  24625  volsup2  24674  itg2seq  24812  itg2cn  24833  tdeglem4  25129  tdeglem4OLD  25130  aaliou3lem9  25415  ftalem7  26133  dchrptlem3  26319  dchrsum2  26321  tglowdim1i  26766  tglowdim2ln  26916  brbtwn2  27176  colinearalg  27181  axlowdimlem6  27218  axlowdimlem14  27226  umgr2edg1  27481  umgr2edgneu  27484  nfrgr2v  28537  4cycl2vnunb  28555  nmounbi  29039  nmobndseqi  29042  minvecolem5  29144  fprodex01  31041  xrnarchi  31340  isarchi2  31341  ssmxidllem  31543  fedgmullem2  31613  ordtconnlem1  31776  lmdvg  31805  hasheuni  31953  voliune  32097  volfiniune  32098  ballotlemodife  32364  ballotlem4  32365  reprdifc  32507  bnj1542  32737  bnj110  32738  bnj1189  32889  noseponlem  33794  nolt02o  33825  noetasuplem4  33866  noetainflem4  33870  cofcutr  34019  dfrecs2  34179  brub  34183  filnetlem4  34497  unblimceq0  34614  relowlpssretop  35462  nlpineqsn  35506  matunitlindflem1  35700  poimirlem23  35727  poimirlem30  35734  poimirlem32  35736  poimir  35737  mblfinlem1  35741  aks4d1p3  40014  aks4d1p8d2  40021  dffltz  40387  infdesc  40396  fphpd  40554  fiphp3d  40557  rencldnfilem  40558  pellfundglb  40623  clsk3nimkb  41539  ndisj2  42488  eliin2f  42543  infrpge  42780  infxrbnd2  42798  supminfxr  42894  limcrecl  43060  limsupub  43135  limsuppnflem  43141  limsupre2lem  43155  stoweidlem14  43445  stoweidlem34  43465  salexct  43763  meaiuninc3v  43912  vonioo  44110  vonicc  44113  copisnmnd  45251  zrninitoringc  45517  pgrpgt2nabl  45590  islindeps  45682  islininds2  45713  ldepslinc  45738  line2ylem  45985  line2xlem  45987