Theorem rexnal 3116

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3078  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3079  df-rex 3089

This theorem is used by:  r19.35  3122  r19.30  3131  rexnal2  3146  rexnal3  3147  raleq  3318  elpwunsn  4648  n0snor2el  4796  uni0b  4897  iundif2  5036  weniso  7361  rexrnmpo  7557  onnseq  8337  cofonr  8666  ixp0  8942  boxcutc  8952  isfinite2  9272  ordtypelem9  9502  ordtypelem10  9503  unbndrank  9828  tcrank  9870  infxpenlem  10020  kmlem3  10159  kmlem7  10163  kmlem8  10164  kmlem13  10169  cfeq0  10262  isf32lem2  10360  isf32lem5  10363  isf34lem4  10383  fin1a2lem7  10412  ac6n  10491  alephval2  10585  pwfseqlem3  10673  inttsk  10787  nqereu  10942  npomex  11009  prlem934  11046  arch  12529  qextlt  13259  qextle  13260  xralrple  13261  xrsupsslem  13363  xrinfmsslem  13364  supxrbnd1  13377  supxrbnd2  13378  supxrbnd  13384  fsuppmapnn0fiubex  14060  hashfun  14506  hashge2el2dif  14549  limsuplt  15570  fprodle  16089  alzdvds  16416  isprm5  16804  ncoprmlnprm  16825  pc2dvds  16977  vdwnn  17096  ramcl  17127  cshwshashlem1  17193  cshwshash  17202  isnsgrp  18831  isnmnd  18846  smndex1n0mnd  19030  lt6abl  20028  simpgnideld  20234  zrninitoringc  20844  ssdifidllem  21553  psdmul  22400  mdetunilem8  22847  matunitlindflem1  22907  fctop  23235  cctop  23237  t0dist  23556  ist0-3  23576  pthaus  23870  txkgen  23884  xkohaus  23885  fbfinnfr  24073  isufil2  24140  hausflim  24213  fclscf  24257  bcth  25563  minveclem3b  25662  pmltpc  25684  volsup  25790  volsup2  25839  itg2seq  25976  itg2cn  25997  tdeglem4  26292  rnplynfin  26546  plyconz  26547  aaliou3lem9  26593  ftalem7  27323  dchrptlem3  27510  dchrsum2  27512  noseponlem  27908  nolt02o  27939  noetasuplem4  27980  noetainflem4  27984  cofcutr  28197  tglowdim1i  28851  tglowdim2ln  29007  brbtwn2  29370  colinearalg  29375  axlowdimlem6  29412  axlowdimlem14  29420  umgr2edg1  29679  umgr2edgneu  29682  nfrgr2v  30760  4cycl2vnunb  30778  nmounbi  31265  nmobndseqi  31268  minvecolem5  31370  fprodex01  33303  xrnarchi  33632  isarchi2  33633  mxidlirred  33883  ssmxidllem  33884  fedgmullem2  34148  ordtconnlem1  34442  lmdvg  34471  hasheuni  34603  voliune  34748  volfiniune  34749  ballotlemodife  35017  ballotlem4  35018  reprdifc  35143  bnj1542  35374  bnj110  35375  bnj1189  35526  noinfepregs  35667  dfrecs2  36537  brub  36541  ltnadd  36806  naddle  36807  filnetlem4  37008  unblimceq0  37212  relowlpssretop  38126  nlpineqsn  38170  poimirlem23  38400  poimirlem30  38407  poimirlem32  38409  poimir  38410  mblfinlem1  38414  aks4d1p3  42952  aks4d1p8d2  42959  aks6d1c2p2  42993  aks6d1c5  43013  dffltz  43488  infdesc  43497  fphpd  43665  fiphp3d  43668  rencldnfilem  43669  pellfundglb  43734  onmaxnelsup  44072  onsupnmax  44077  ralopabb  44259  clsk3nimkb  44888  ndisj2  45893  eliin2f  45944  infrpge  46189  infxrbnd2  46206  supminfxr  46300  rexanuz2nf  46328  limcrecl  46467  limsupub  46540  limsuppnflem  46546  limsupre2lem  46560  stoweidlem14  46850  stoweidlem34  46870  salexct  47170  meaiuninc3v  47320  vonioo  47518  vonicc  47521  copisnmnd  49092  pgrpgt2nabl  49304  islindeps  49391  islininds2  49422  ldepslinc  49447  line2ylem  49689  line2xlem  49691  iineq0  49756  nelsubclem  50001  setc1onsubc  50536