Theorem rexnal 3185

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

Syntax hints:  ¬ wn 3   ↔ wb 198  ∀wral 3088  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-ral 3093  df-rex 3094

This theorem is referenced by:  rexnal2  3204  rexnal3  3205  r19.35  3282  2ralor  3310  elpwunsn  4496  n0snor2el  4639  uni0b  4738  iundif2  4863  weniso  6932  rexrnmpo  7108  onnseq  7787  ixp0  8294  boxcutc  8304  isfinite2  8573  ordtypelem9  8787  ordtypelem10  8788  unbndrank  9067  tcrank  9109  infxpenlem  9235  kmlem3  9374  kmlem7  9378  kmlem8  9379  kmlem13  9384  cfeq0  9478  isf32lem2  9576  isf32lem5  9579  isf34lem4  9599  fin1a2lem7  9628  ac6n  9707  alephval2  9794  pwfseqlem3  9882  inttsk  9996  nqereu  10151  npomex  10218  prlem934  10255  arch  11707  qextlt  12416  qextle  12417  xralrple  12418  xrsupsslem  12519  xrinfmsslem  12520  supxrbnd1  12533  supxrbnd2  12534  supxrbnd  12540  fsuppmapnn0fiubex  13178  hashfun  13614  hashge2el2dif  13652  limsuplt  14700  fprodle  15213  alzdvds  15533  isprm5  15910  ncoprmlnprm  15927  pc2dvds  16074  vdwnn  16193  ramcl  16224  cshwshashlem1  16288  cshwshash  16297  isnsgrp  17759  isnmnd  17769  lt6abl  18772  mdetunilem8  20935  fctop  21319  cctop  21321  t0dist  21640  ist0-3  21660  pthaus  21953  txkgen  21967  xkohaus  21968  fbfinnfr  22156  isufil2  22223  hausflim  22296  fclscf  22340  bcth  23638  minveclem3b  23737  pmltpc  23757  volsup  23863  volsup2  23912  itg2seq  24049  itg2cn  24070  tdeglem4  24360  aaliou3lem9  24645  ftalem7  25361  dchrptlem3  25547  dchrsum2  25549  tglowdim1i  25992  tglowdim2ln  26142  brbtwn2  26397  colinearalg  26402  axlowdimlem6  26439  axlowdimlem14  26447  umgr2edg1  26699  umgr2edgneu  26702  nfrgr2v  27809  4cycl2vnunb  27827  nmounbi  28333  nmobndseqi  28336  minvecolem5  28439  fprodex01  30290  xrnarchi  30479  isarchi2  30480  fedgmullem2  30655  ordtconnlem1  30811  lmdvg  30840  hasheuni  30988  voliune  31133  volfiniune  31134  ballotlemodife  31401  ballotlem4  31402  reprdifc  31546  bnj1542  31776  bnj110  31777  bnj1189  31926  noseponlem  32692  nolt02o  32720  noetalem3  32740  dfrecs2  32932  brub  32936  filnetlem4  33250  unblimceq0  33366  relowlpssretop  34087  nlpineqsn  34130  matunitlindflem1  34329  poimirlem23  34356  poimirlem30  34363  poimirlem32  34365  poimir  34366  mblfinlem1  34370  dffltz  38678  fphpd  38809  fiphp3d  38812  rencldnfilem  38813  pellfundglb  38878  clsk3nimkb  39753  simpgnideld  40033  ndisj2  40733  eliin2f  40794  infrpge  41049  infxrbnd2  41067  supminfxr  41172  limcrecl  41342  limsupub  41417  limsuppnflem  41423  limsupre2lem  41437  stoweidlem14  41731  stoweidlem34  41751  salexct  42049  meaiuninc3v  42198  vonioo  42396  vonicc  42399  copisnmnd  43445  zrninitoringc  43707  pgrpgt2nabl  43781  islindeps  43876  islininds2  43907  ldepslinc  43932  line2ylem  44107  line2xlem  44109