Theorem ralnex 3089

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by BJ, 16-Jul-2021.)

Assertion

Ref	Expression
ralnex	⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Proof of Theorem ralnex

Step	Hyp	Ref	Expression
1		raln 3086	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1802	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3088	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 337	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 277	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399  ∀wal 1559  ∃wex 1800   ∈ wcel 2143  ∀wral 3077  ∃wrex 3087

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-ral 3078  df-rex 3088

This theorem is referenced by:  dfrex2  3090  nrex  3091  rexim  3104  dfral2  3114  ralinexa  3116  r19.43  3131  ralnex2  3143  ralnex3  3144  nrexralim  3147  nrexdv  3158  nelb  3239  cbvrexdva  3244  cbvrexfw  3304  cbvrexdva2  3340  rexeqf  3345  rexprg  4657  n0snor2el  4792  iindif2  5035  rexiunxp  5813  rexxpf  5820  nelrnmpt  5944  f0rn0  6750  ordunisuc2  7825  tfi  7834  resf1extb  7916  releldmdifi  8027  omeulem1  8552  frfi  9230  isfinite2  9243  supmo  9399  infmo  9444  ordtypelem9  9475  elirrvOLDOLD  9548  unbndrank  9801  kmlem7  10114  kmlem8  10115  kmlem13  10120  isfin1-3  10344  ac6num  10437  zorn2lem4  10457  fpwwe2lem11  10600  npomex  10955  suplem2pr  11012  dedekind  11347  suprnub  12158  infregelb  12177  arch  12479  xrsupsslem  13311  xrinfmsslem  13312  supxrbnd1  13325  supxrbnd2  13326  supxrleub  13330  supxrbnd  13332  infxrgelb  13340  injresinjlem  13797  hashgt12el  14436  hashgt12el2  14437  sqrt2irr  16282  prmind2  16720  vdwnnlem3  17034  vdwnn  17035  acsfiindd  18586  isnmnd  18773  isnirred  20470  lssne0  21019  bwth  23471  t1connperf  23497  trfbas  23905  fbunfip  23930  fbasrn  23945  filuni  23946  hausflim  24042  alexsubALTlem3  24110  alexsubALTlem4  24111  ptcmplem4  24116  lebnumlem3  25026  bcthlem4  25390  bcth3  25394  amgm  27056  issqf  27201  ostth  27704  nosupbnd1lem4  27776  noinfbnd1lem4  27791  ltsrec  27895  cuteq1  27911  tglowdim2ln  28822  axcontlem12  29177  umgrnloop0  29311  numedglnl  29346  usgrnloop0ALT  29407  uhgrnbgr0nb  29556  nbgr0edg  29559  vtxd0nedgb  29690  vtxdusgr0edgnelALT  29698  1hevtxdg0  29707  usgrvd0nedg  29735  uhgrvd00  29736  pthdlem2lem  29968  nmounbi  30980  lnon0  31002  largei  32471  cvbr2  32487  chrelat2i  32569  n0nsnel  32715  uniinn0  32751  infxrge0gelb  32969  nn0min  33024  toslublem  33151  tosglblem  33153  archiabl  33379  lmdvg  34251  esumcvgre  34389  eulerpartlems  34658  bnj110  35154  bnj1417  35337  fineqvnttrclselem1  35418  lfuhgr3  35471  fmlaomn0  35741  fmla0disjsuc  35749  fmlasucdisj  35750  dfon2lem8  36139  dfint3  36303  bj-axseprep  37560  relowlpssretop  37859  domalom  37899  fvineqsneq  37907  poimirlem26  38146  poimirlem30  38150  poimir  38153  mblfinlem1  38157  ftc1anc  38201  heiborlem1  38311  lcvbr2  39647  lcvbr3  39648  cvrnbtwn  39896  cvrval2  39899  hlrelat2  40028  cdleme0nex  40915  aks4d1p7  42701  sticksstones1  42764  infdesc  43226  nna4b4nsq  43243  rencldnfilem  43398  setindtr  43602  onmaxnelsup  43801  onsupnmax  43806  onsupmaxb  43817  onsupeqnmax  43825  ordnexbtwnsuc  43845  gneispace  44711  iindif2f  45739  ralfal  45740  supxrgere  45910  supxrgelem  45914  infxrbnd2  45945  supminfxr  46039  limsupub  46279  limsuppnflem  46285  limsupre2lem  46299  stirlinglem5  46653  etransclem24  46833  etransclem32  46841  sge0iunmpt  46993  sge0rpcpnf  46996  iundjiun  47035  voliunsge0lem  47047  meaiuninc3v  47059  meaiininclem  47061  hoidmv1lelem3  47168  hoidmvlelem4  47173  hoidmvlelem5  47174  n0nsn2el  47620  0nelsetpreimafv  47997  nprmmul1  48134  stgr0  48583  gpg5nbgrvtx03starlem1  48691  gpg5nbgrvtx03starlem2  48692  gpg5nbgrvtx03starlem3  48693  gpg5nbgrvtx13starlem1  48694  gpg5nbgrvtx13starlem2  48695  gpg5nbgrvtx13starlem3  48696  gpg5edgnedg  48753  copisnmnd  48792  lindslinindsimp1  49080  lindslinindsimp2  49086  ldepslinc  49132  aacllem  50423