Theorem rexnal 3117

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3079  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-ral 3080  df-rex 3090

This theorem is referenced by:  r19.35  3123  r19.30  3132  rexnal2  3147  rexnal3  3148  raleq  3320  elpwunsn  4646  n0snor2el  4793  uni0b  4894  iundif2  5033  weniso  7342  rexrnmpo  7540  onnseq  8319  cofonr  8648  ixp0  8917  boxcutc  8927  isfinite2  9246  ordtypelem9  9476  ordtypelem10  9477  unbndrank  9802  tcrank  9844  infxpenlem  9985  kmlem3  10124  kmlem7  10128  kmlem8  10129  kmlem13  10134  cfeq0  10228  isf32lem2  10326  isf32lem5  10329  isf34lem4  10349  fin1a2lem7  10378  ac6n  10457  alephval2  10545  pwfseqlem3  10633  inttsk  10747  nqereu  10902  npomex  10969  prlem934  11006  arch  12489  qextlt  13217  qextle  13218  xralrple  13219  xrsupsslem  13321  xrinfmsslem  13322  supxrbnd1  13335  supxrbnd2  13336  supxrbnd  13342  fsuppmapnn0fiubex  14016  hashfun  14462  hashge2el2dif  14505  limsuplt  15518  fprodle  16038  alzdvds  16366  isprm5  16754  ncoprmlnprm  16775  pc2dvds  16927  vdwnn  17046  ramcl  17077  cshwshashlem1  17143  cshwshash  17152  isnsgrp  18769  isnmnd  18784  smndex1n0mnd  18962  lt6abl  19953  simpgnideld  20159  zrninitoringc  20749  ssdifidllem  21441  psdmul  22286  mdetunilem8  22733  fctop  23118  cctop  23120  t0dist  23439  ist0-3  23459  pthaus  23752  txkgen  23766  xkohaus  23767  fbfinnfr  23955  isufil2  24022  hausflim  24095  fclscf  24139  bcth  25445  minveclem3b  25544  pmltpc  25566  volsup  25672  volsup2  25721  itg2seq  25858  itg2cn  25879  tdeglem4  26174  aaliou3lem9  26468  ftalem7  27197  dchrptlem3  27384  dchrsum2  27386  noseponlem  27782  nolt02o  27813  noetasuplem4  27854  noetainflem4  27858  cofcutr  28071  tglowdim1i  28724  tglowdim2ln  28875  brbtwn2  29160  colinearalg  29165  axlowdimlem6  29202  axlowdimlem14  29210  umgr2edg1  29466  umgr2edgneu  29469  nfrgr2v  30528  4cycl2vnunb  30546  nmounbi  31033  nmobndseqi  31036  minvecolem5  31138  fprodex01  33077  xrnarchi  33412  isarchi2  33413  mxidlirred  33667  ssmxidllem  33668  fedgmullem2  33932  ordtconnlem1  34226  lmdvg  34255  hasheuni  34387  voliune  34531  volfiniune  34532  ballotlemodife  34800  ballotlem4  34801  reprdifc  34926  bnj1542  35157  bnj110  35158  bnj1189  35309  noinfepregs  35436  dfrecs2  36308  brub  36312  filnetlem4  36749  unblimceq0  36953  relowlpssretop  37865  nlpineqsn  37909  matunitlindflem1  38122  poimirlem23  38149  poimirlem30  38156  poimirlem32  38158  poimir  38159  mblfinlem1  38163  aks4d1p3  42702  aks4d1p8d2  42709  aks6d1c2p2  42743  aks6d1c5  42763  dffltz  43223  infdesc  43232  fphpd  43400  fiphp3d  43403  rencldnfilem  43404  pellfundglb  43469  onmaxnelsup  43807  onsupnmax  43812  ralopabb  43994  clsk3nimkb  44623  ndisj2  45630  eliin2f  45681  infrpge  45926  infxrbnd2  45943  supminfxr  46037  rexanuz2nf  46065  limcrecl  46204  limsupub  46277  limsuppnflem  46283  limsupre2lem  46297  stoweidlem14  46587  stoweidlem34  46607  salexct  46907  meaiuninc3v  47057  vonioo  47255  vonicc  47258  copisnmnd  48790  pgrpgt2nabl  48998  islindeps  49085  islininds2  49116  ldepslinc  49141  line2ylem  49383  line2xlem  49385  iineq0  49450  nelsubclem  49697  setc1onsubc  50232