Theorem rexnal 3113

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

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wral 3075  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ral 3076  df-rex 3086

This theorem is referenced by:  r19.35  3119  r19.30  3128  rexnal2  3143  rexnal3  3144  raleq  3316  elpwunsn  4640  n0snor2el  4788  uni0b  4889  iundif2  5028  weniso  7332  rexrnmpo  7530  onnseq  8308  cofonr  8637  ixp0  8906  boxcutc  8916  isfinite2  9235  ordtypelem9  9467  ordtypelem10  9468  unbndrank  9793  tcrank  9835  infxpenlem  9962  kmlem3  10102  kmlem7  10106  kmlem8  10107  kmlem13  10112  cfeq0  10206  isf32lem2  10304  isf32lem5  10307  isf34lem4  10327  fin1a2lem7  10356  ac6n  10435  alephval2  10523  pwfseqlem3  10611  inttsk  10725  nqereu  10880  npomex  10947  prlem934  10984  arch  12471  qextlt  13199  qextle  13200  xralrple  13201  xrsupsslem  13303  xrinfmsslem  13304  supxrbnd1  13317  supxrbnd2  13318  supxrbnd  13324  fsuppmapnn0fiubex  13998  hashfun  14443  hashge2el2dif  14486  limsuplt  15496  fprodle  16016  alzdvds  16344  isprm5  16732  ncoprmlnprm  16753  pc2dvds  16905  vdwnn  17024  ramcl  17055  cshwshashlem1  17121  cshwshash  17130  isnsgrp  18747  isnmnd  18762  smndex1n0mnd  18939  lt6abl  19925  simpgnideld  20131  zrninitoringc  20712  psdmul  22218  mdetunilem8  22666  fctop  23051  cctop  23053  t0dist  23372  ist0-3  23392  pthaus  23685  txkgen  23699  xkohaus  23700  fbfinnfr  23888  isufil2  23955  hausflim  24028  fclscf  24072  bcth  25378  minveclem3b  25477  pmltpc  25499  volsup  25605  volsup2  25654  itg2seq  25791  itg2cn  25812  tdeglem4  26107  aaliou3lem9  26401  ftalem7  27130  dchrptlem3  27317  dchrsum2  27319  noseponlem  27715  nolt02o  27746  noetasuplem4  27787  noetainflem4  27791  cofcutr  28004  tglowdim1i  28657  tglowdim2ln  28807  brbtwn2  29062  colinearalg  29067  axlowdimlem6  29104  axlowdimlem14  29112  umgr2edg1  29368  umgr2edgneu  29371  nfrgr2v  30430  4cycl2vnunb  30448  nmounbi  30935  nmobndseqi  30938  minvecolem5  31040  fprodex01  32987  xrnarchi  33324  isarchi2  33325  ssdifidllem  33603  mxidlirred  33620  ssmxidllem  33621  fedgmullem2  33887  ordtconnlem1  34181  lmdvg  34210  hasheuni  34342  voliune  34486  volfiniune  34487  ballotlemodife  34755  ballotlem4  34756  reprdifc  34881  bnj1542  35112  bnj110  35113  bnj1189  35264  noinfepregs  35389  dfrecs2  36260  brub  36264  filnetlem4  36701  unblimceq0  36905  relowlpssretop  37818  nlpineqsn  37862  matunitlindflem1  38075  poimirlem23  38102  poimirlem30  38109  poimirlem32  38111  poimir  38112  mblfinlem1  38116  aks4d1p3  42655  aks4d1p8d2  42662  aks6d1c2p2  42696  aks6d1c5  42716  dffltz  43176  infdesc  43185  fphpd  43353  fiphp3d  43356  rencldnfilem  43357  pellfundglb  43422  onmaxnelsup  43760  onsupnmax  43765  ralopabb  43947  clsk3nimkb  44576  ndisj2  45591  eliin2f  45642  infrpge  45887  infxrbnd2  45904  supminfxr  45998  rexanuz2nf  46026  limcrecl  46165  limsupub  46238  limsuppnflem  46244  limsupre2lem  46258  stoweidlem14  46548  stoweidlem34  46568  salexct  46868  meaiuninc3v  47018  vonioo  47216  vonicc  47219  copisnmnd  48751  pgrpgt2nabl  48948  islindeps  49035  islininds2  49066  ldepslinc  49091  line2ylem  49333  line2xlem  49335  iineq0  49401  nelsubclem  49648  setc1onsubc  50183