Theorem ralnex 3163

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 3080	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1785	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3069	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 334	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 274	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395  ∀wal 1537  ∃wex 1783   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  dfral2  3164  dfrex2  3166  ralnex2  3188  ralnex3  3189  ralinexa  3190  nrexralim  3192  nelb  3194  nelbOLD  3195  nrex  3196  nrexdv  3197  r19.30OLD  3266  r19.43  3277  rexeqbidvv  3330  rexprg  4629  n0snor2el  4761  iindif2  5002  rexiunxp  5738  rexxpf  5745  f0rn0  6643  ordunisuc2  7666  tfi  7675  releldmdifi  7859  omeulem1  8375  frfi  8989  isfinite2  9002  supmo  9141  infmo  9184  ordtypelem9  9215  elirrv  9285  unbndrank  9531  kmlem7  9843  kmlem8  9844  kmlem13  9849  isfin1-3  10073  ac6num  10166  zorn2lem4  10186  fpwwe2lem11  10328  npomex  10683  suplem2pr  10740  dedekind  11068  suprnub  11870  infregelb  11889  arch  12160  xrsupsslem  12970  xrinfmsslem  12971  supxrbnd1  12984  supxrbnd2  12985  supxrleub  12989  supxrbnd  12991  infxrgelb  12998  injresinjlem  13435  hashgt12el  14065  hashgt12el2  14066  sqrt2irr  15886  prmind2  16318  vdwnnlem3  16626  vdwnn  16627  acsfiindd  18186  isnmnd  18304  isnirred  19857  lssne0  20127  bwth  22469  t1connperf  22495  trfbas  22903  fbunfip  22928  fbasrn  22943  filuni  22944  hausflim  23040  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem4  23114  lebnumlem3  24032  bcthlem4  24396  bcth3  24400  amgm  26045  issqf  26190  ostth  26692  tglowdim2ln  26916  axcontlem12  27246  umgrnloop0  27382  numedglnl  27417  usgrnloop0ALT  27475  uhgrnbgr0nb  27624  nbgr0edg  27627  vtxd0nedgb  27758  vtxdusgr0edgnelALT  27766  1hevtxdg0  27775  usgrvd0nedg  27803  uhgrvd00  27804  pthdlem2lem  28036  nmounbi  29039  lnon0  29061  largei  30530  cvbr2  30546  chrelat2i  30628  uniinn0  30791  infxrge0gelb  30991  nn0min  31036  toslublem  31152  tosglblem  31154  archiabl  31354  lmdvg  31805  esumcvgre  31959  eulerpartlems  32227  bnj110  32738  bnj1417  32921  lfuhgr3  32981  fmlaomn0  33252  fmla0disjsuc  33260  fmlasucdisj  33261  dfon2lem8  33672  nosupbnd1lem4  33841  noinfbnd1lem4  33856  sltrec  33941  dfint3  34181  relowlpssretop  35462  domalom  35502  fvineqsneq  35510  poimirlem26  35730  poimirlem30  35734  poimir  35737  mblfinlem1  35741  ftc1anc  35785  heiborlem1  35896  lcvbr2  36963  lcvbr3  36964  cvrnbtwn  37212  cvrval2  37215  hlrelat2  37344  cdleme0nex  38231  aks4d1p7  40019  sticksstones1  40030  infdesc  40396  nna4b4nsq  40413  rencldnfilem  40558  setindtr  40762  gneispace  41633  nelrnmpt  42523  supxrgere  42762  supxrgelem  42766  infxrbnd2  42798  supminfxr  42894  limsupub  43135  limsuppnflem  43141  limsupre2lem  43155  stirlinglem5  43509  etransclem24  43689  etransclem32  43697  sge0iunmpt  43846  sge0rpcpnf  43849  iundjiun  43888  voliunsge0lem  43900  meaiuninc3v  43912  meaiininclem  43914  hoidmv1lelem3  44021  hoidmvlelem4  44026  hoidmvlelem5  44027  0nelsetpreimafv  44730  copisnmnd  45251  lindslinindsimp1  45686  lindslinindsimp2  45692  ldepslinc  45738  aacllem  46391