Theorem ralnex 3073

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 3070	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1784	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3072	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 275	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397  ∀wal 1540  ∃wex 1782   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063  df-rex 3072

This theorem is referenced by:  dfrex2  3074  nrex  3075  rexim  3088  dfral2  3100  ralinexa  3102  r19.30OLD  3122  r19.43  3123  ralnex2  3134  ralnex3  3135  nrexralim  3138  nrexdv  3150  nelb  3232  nelbOLD  3233  cbvrexdva  3238  cbvrexfw  3303  rexeqbidvvOLD  3333  cbvrexdva2  3346  rexeqf  3351  rexprg  4700  n0snor2el  4834  iindif2  5080  rexiunxp  5839  rexxpf  5846  f0rn0  6774  ordunisuc2  7830  tfi  7839  releldmdifi  8028  omeulem1  8579  frfi  9285  isfinite2  9298  supmo  9444  infmo  9487  ordtypelem9  9518  elirrv  9588  unbndrank  9834  kmlem7  10148  kmlem8  10149  kmlem13  10154  isfin1-3  10378  ac6num  10471  zorn2lem4  10491  fpwwe2lem11  10633  npomex  10988  suplem2pr  11045  dedekind  11374  suprnub  12176  infregelb  12195  arch  12466  xrsupsslem  13283  xrinfmsslem  13284  supxrbnd1  13297  supxrbnd2  13298  supxrleub  13302  supxrbnd  13304  infxrgelb  13311  injresinjlem  13749  hashgt12el  14379  hashgt12el2  14380  sqrt2irr  16189  prmind2  16619  vdwnnlem3  16927  vdwnn  16928  acsfiindd  18503  isnmnd  18626  isnirred  20227  lssne0  20554  bwth  22906  t1connperf  22932  trfbas  23340  fbunfip  23365  fbasrn  23380  filuni  23381  hausflim  23477  alexsubALTlem3  23545  alexsubALTlem4  23546  ptcmplem4  23551  lebnumlem3  24471  bcthlem4  24836  bcth3  24840  amgm  26485  issqf  26630  ostth  27132  nosupbnd1lem4  27204  noinfbnd1lem4  27219  sltrec  27311  cuteq1  27324  tglowdim2ln  27892  axcontlem12  28223  umgrnloop0  28359  numedglnl  28394  usgrnloop0ALT  28452  uhgrnbgr0nb  28601  nbgr0edg  28604  vtxd0nedgb  28735  vtxdusgr0edgnelALT  28743  1hevtxdg0  28752  usgrvd0nedg  28780  uhgrvd00  28781  pthdlem2lem  29014  nmounbi  30017  lnon0  30039  largei  31508  cvbr2  31524  chrelat2i  31606  uniinn0  31770  infxrge0gelb  31967  nn0min  32014  toslublem  32130  tosglblem  32132  archiabl  32332  lmdvg  32922  esumcvgre  33078  eulerpartlems  33348  bnj110  33858  bnj1417  34041  lfuhgr3  34099  fmlaomn0  34370  fmla0disjsuc  34378  fmlasucdisj  34379  dfon2lem8  34751  dfint3  34913  relowlpssretop  36234  domalom  36274  fvineqsneq  36282  poimirlem26  36503  poimirlem30  36507  poimir  36510  mblfinlem1  36514  ftc1anc  36558  heiborlem1  36668  lcvbr2  37881  lcvbr3  37882  cvrnbtwn  38130  cvrval2  38133  hlrelat2  38263  cdleme0nex  39150  aks4d1p7  40937  sticksstones1  40951  infdesc  41382  nna4b4nsq  41399  rencldnfilem  41544  setindtr  41749  onmaxnelsup  41958  onsupnmax  41963  onsupmaxb  41974  onsupeqnmax  41982  ordnexbtwnsuc  42003  gneispace  42871  nelrnmpt  43759  iindif2f  43840  ralfal  43841  supxrgere  44030  supxrgelem  44034  infxrbnd2  44066  supminfxr  44161  limsupub  44407  limsuppnflem  44413  limsupre2lem  44427  stirlinglem5  44781  etransclem24  44961  etransclem32  44969  sge0iunmpt  45121  sge0rpcpnf  45124  iundjiun  45163  voliunsge0lem  45175  meaiuninc3v  45187  meaiininclem  45189  hoidmv1lelem3  45296  hoidmvlelem4  45301  hoidmvlelem5  45302  n0nsn2el  45722  0nelsetpreimafv  46045  copisnmnd  46566  lindslinindsimp1  47092  lindslinindsimp2  47098  ldepslinc  47144  aacllem  47802