Theorem ralnex 3093

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 3090	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1814	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3092	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 338	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091

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 3082  df-rex 3092

This theorem is used by:  dfrex2  3094  nrex  3095  rexim  3108  dfral2  3118  ralinexa  3120  r19.43  3135  ralnex2  3147  ralnex3  3148  nrexralim  3151  nrexdv  3162  nelb  3243  cbvrexdva  3248  cbvrexfw  3308  cbvrexdva2  3343  rexeqf  3348  rexprg  4665  n0snor2el  4800  iindif2  5045  rexiunxp  5828  rexxpf  5835  nelrnmpt  5959  f0rn0  6767  ordunisuc2  7846  tfi  7855  resf1extb  7937  releldmdifi  8048  omeulem1  8573  frfi  9252  isfinite2  9265  supmo  9419  infmo  9464  ordtypelem9  9495  elirrvOLDOLD  9568  unbndrank  9821  kmlem7  10156  kmlem8  10157  kmlem13  10162  isfin1-3  10385  ac6num  10478  zorn2lem4  10498  fpwwe2lem11  10643  npomex  10998  suplem2pr  11055  dedekind  11390  suprnub  12197  infregelb  12216  arch  12518  xrsupsslem  13351  xrinfmsslem  13352  supxrbnd1  13365  supxrbnd2  13366  supxrleub  13370  supxrbnd  13372  infxrgelb  13380  injresinjlem  13838  hashgt12el  14479  hashgt12el2  14480  sqrt2irr  16329  prmind2  16767  vdwnnlem3  17081  vdwnn  17082  acsfiindd  18633  isnmnd  18830  isnirred  20550  lssne0  21124  bwth  23619  t1connperf  23645  trfbas  24054  fbunfip  24079  fbasrn  24094  filuni  24095  hausflim  24191  alexsubALTlem3  24259  alexsubALTlem4  24260  ptcmplem4  24265  lebnumlem3  25175  bcthlem4  25539  bcth3  25543  amgm  27208  issqf  27353  ostth  27856  nosupbnd1lem4  27928  noinfbnd1lem4  27943  ltsrec  28047  cuteq1  28063  tglowdim2ln  28978  axcontlem12  29382  umgrnloop0  29516  numedglnl  29551  lfuhgr3  29557  usgrnloop0ALT  29615  uhgrnbgr0nb  29764  nbgr0edg  29767  vtxd0nedgb  29898  vtxdusgr0edgnelALT  29906  1hevtxdg0  29915  usgrvd0nedg  29943  uhgrvd00  29944  pthdlem2lem  30182  nmounbi  31201  lnon0  31223  largei  32692  cvbr2  32708  chrelat2i  32790  n0nsnel  32934  uniinn0  32970  infxrge0gelb  33183  nn0min  33237  toslublem  33358  tosglblem  33360  archiabl  33584  lmdvg  34409  esumcvgre  34547  eulerpartlems  34817  bnj110  35313  bnj1417  35496  fineqvnttrclselem1  35593  fmlaomn0  35921  fmla0disjsuc  35929  fmlasucdisj  35930  dfon2lem8  36319  dfint3  36483  bj-axseprep  37770  relowlpssretop  38069  domalom  38109  fvineqsneq  38117  poimirlem26  38356  poimirlem30  38360  poimir  38363  mblfinlem1  38367  ftc1anc  38411  heiborlem1  38522  lcvbr2  39856  lcvbr3  39857  cvrnbtwn  40105  cvrval2  40108  hlrelat2  40237  cdleme0nex  41124  aks4d1p7  42910  sticksstones1  42973  infdesc  43435  nna4b4nsq  43452  rencldnfilem  43607  setindtr  43811  onmaxnelsup  44010  onsupnmax  44015  onsupmaxb  44026  onsupeqnmax  44034  ordnexbtwnsuc  44054  gneispace  44920  iindif2f  45938  ralfal  45939  supxrgere  46109  supxrgelem  46113  infxrbnd2  46144  supminfxr  46238  limsupub  46478  limsuppnflem  46484  limsupre2lem  46498  stirlinglem5  46852  etransclem24  47032  etransclem32  47040  sge0iunmpt  47192  sge0rpcpnf  47195  iundjiun  47234  voliunsge0lem  47246  meaiuninc3v  47258  meaiininclem  47260  hoidmv1lelem3  47367  hoidmvlelem4  47372  hoidmvlelem5  47373  n0nsn2el  47822  0nelsetpreimafv  48199  nprmmul1  48336  stgr0  48785  gpg5nbgrvtx03starlem1  48893  gpg5nbgrvtx03starlem2  48894  gpg5nbgrvtx03starlem3  48895  gpg5nbgrvtx13starlem1  48896  gpg5nbgrvtx13starlem2  48897  gpg5nbgrvtx13starlem3  48898  gpg5edgnedg  48955  copisnmnd  48993  lindslinindsimp1  49296  lindslinindsimp2  49302  ldepslinc  49348  aacllem  50680