Theorem ralnex 3055

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  dfrex2  3056  nrex  3057  rexim  3070  dfral2  3081  ralinexa  3083  r19.43  3101  ralnex2  3113  ralnex3  3114  nrexralim  3117  nrexdv  3128  nelb  3211  cbvrexdva  3216  cbvrexfw  3277  rexeqbidvvOLD  3307  cbvrexdva2  3319  rexeqf  3327  rexprg  4657  n0snor2el  4793  iindif2  5036  rexiunxp  5794  rexxpf  5801  f0rn0  6727  ordunisuc2  7800  tfi  7809  resf1extb  7890  releldmdifi  8003  omeulem1  8523  frfi  9208  isfinite2  9221  supmo  9379  infmo  9424  ordtypelem9  9455  elirrv  9525  unbndrank  9771  kmlem7  10086  kmlem8  10087  kmlem13  10092  isfin1-3  10315  ac6num  10408  zorn2lem4  10428  fpwwe2lem11  10570  npomex  10925  suplem2pr  10982  dedekind  11313  suprnub  12124  infregelb  12143  arch  12415  xrsupsslem  13243  xrinfmsslem  13244  supxrbnd1  13257  supxrbnd2  13258  supxrleub  13262  supxrbnd  13264  infxrgelb  13272  injresinjlem  13724  hashgt12el  14363  hashgt12el2  14364  sqrt2irr  16193  prmind2  16631  vdwnnlem3  16944  vdwnn  16945  acsfiindd  18494  isnmnd  18647  isnirred  20340  lssne0  20889  bwth  23330  t1connperf  23356  trfbas  23764  fbunfip  23789  fbasrn  23804  filuni  23805  hausflim  23901  alexsubALTlem3  23969  alexsubALTlem4  23970  ptcmplem4  23975  lebnumlem3  24895  bcthlem4  25260  bcth3  25264  amgm  26934  issqf  27079  ostth  27583  nosupbnd1lem4  27656  noinfbnd1lem4  27671  sltrec  27767  cuteq1  27783  tglowdim2ln  28631  axcontlem12  28955  umgrnloop0  29089  numedglnl  29124  usgrnloop0ALT  29185  uhgrnbgr0nb  29334  nbgr0edg  29337  vtxd0nedgb  29469  vtxdusgr0edgnelALT  29477  1hevtxdg0  29486  usgrvd0nedg  29514  uhgrvd00  29515  pthdlem2lem  29747  nmounbi  30755  lnon0  30777  largei  32246  cvbr2  32262  chrelat2i  32344  n0nsnel  32494  uniinn0  32529  infxrge0gelb  32739  nn0min  32795  toslublem  32944  tosglblem  32946  archiabl  33167  lmdvg  33936  esumcvgre  34074  eulerpartlems  34344  bnj110  34841  bnj1417  35024  lfuhgr3  35100  fmlaomn0  35370  fmla0disjsuc  35378  fmlasucdisj  35379  dfon2lem8  35771  dfint3  35933  relowlpssretop  37345  domalom  37385  fvineqsneq  37393  poimirlem26  37633  poimirlem30  37637  poimir  37640  mblfinlem1  37644  ftc1anc  37688  heiborlem1  37798  lcvbr2  39008  lcvbr3  39009  cvrnbtwn  39257  cvrval2  39260  hlrelat2  39390  cdleme0nex  40277  aks4d1p7  42064  sticksstones1  42127  infdesc  42624  nna4b4nsq  42641  rencldnfilem  42801  setindtr  43006  onmaxnelsup  43205  onsupnmax  43210  onsupmaxb  43221  onsupeqnmax  43229  ordnexbtwnsuc  43249  gneispace  44116  nelrnmpt  45071  iindif2f  45147  ralfal  45148  supxrgere  45322  supxrgelem  45326  infxrbnd2  45358  supminfxr  45453  limsupub  45695  limsuppnflem  45701  limsupre2lem  45715  stirlinglem5  46069  etransclem24  46249  etransclem32  46257  sge0iunmpt  46409  sge0rpcpnf  46412  iundjiun  46451  voliunsge0lem  46463  meaiuninc3v  46475  meaiininclem  46477  hoidmv1lelem3  46584  hoidmvlelem4  46589  hoidmvlelem5  46590  n0nsn2el  47019  0nelsetpreimafv  47384  stgr0  47952  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  copisnmnd  48150  lindslinindsimp1  48439  lindslinindsimp2  48445  ldepslinc  48491  aacllem  49783