Theorem ralnex 3064

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  dfrex2  3065  nrex  3066  rexim  3079  dfral2  3089  ralinexa  3091  r19.43  3106  ralnex2  3118  ralnex3  3119  nrexralim  3122  nrexdv  3133  nelb  3214  cbvrexdva  3219  cbvrexfw  3279  rexeqbidvvOLD  3309  cbvrexdva2  3321  rexeqf  3328  rexprg  4656  n0snor2el  4791  iindif2  5034  rexiunxp  5797  rexxpf  5804  nelrnmpt  5924  f0rn0  6727  ordunisuc2  7796  tfi  7805  resf1extb  7886  releldmdifi  7999  omeulem1  8519  frfi  9197  isfinite2  9210  supmo  9367  infmo  9412  ordtypelem9  9443  elirrvOLD  9515  unbndrank  9766  kmlem7  10079  kmlem8  10080  kmlem13  10085  isfin1-3  10308  ac6num  10401  zorn2lem4  10421  fpwwe2lem11  10564  npomex  10919  suplem2pr  10976  dedekind  11308  suprnub  12119  infregelb  12138  arch  12410  xrsupsslem  13234  xrinfmsslem  13235  supxrbnd1  13248  supxrbnd2  13249  supxrleub  13253  supxrbnd  13255  infxrgelb  13263  injresinjlem  13718  hashgt12el  14357  hashgt12el2  14358  sqrt2irr  16186  prmind2  16624  vdwnnlem3  16937  vdwnn  16938  acsfiindd  18488  isnmnd  18675  isnirred  20371  lssne0  20917  bwth  23369  t1connperf  23395  trfbas  23803  fbunfip  23828  fbasrn  23843  filuni  23844  hausflim  23940  alexsubALTlem3  24008  alexsubALTlem4  24009  ptcmplem4  24014  lebnumlem3  24933  bcthlem4  25298  bcth3  25302  amgm  26972  issqf  27117  ostth  27621  nosupbnd1lem4  27694  noinfbnd1lem4  27709  ltsrec  27812  cuteq1  27828  tglowdim2ln  28739  axcontlem12  29064  umgrnloop0  29198  numedglnl  29233  usgrnloop0ALT  29294  uhgrnbgr0nb  29443  nbgr0edg  29446  vtxd0nedgb  29578  vtxdusgr0edgnelALT  29586  1hevtxdg0  29595  usgrvd0nedg  29623  uhgrvd00  29624  pthdlem2lem  29856  nmounbi  30868  lnon0  30890  largei  32359  cvbr2  32375  chrelat2i  32457  n0nsnel  32606  uniinn0  32641  infxrge0gelb  32861  nn0min  32916  toslublem  33069  tosglblem  33071  archiabl  33296  lmdvg  34135  esumcvgre  34273  eulerpartlems  34542  bnj110  35038  bnj1417  35221  fineqvnttrclselem1  35303  lfuhgr3  35340  fmlaomn0  35610  fmla0disjsuc  35618  fmlasucdisj  35619  dfon2lem8  36008  dfint3  36172  bj-axseprep  37326  relowlpssretop  37623  domalom  37663  fvineqsneq  37671  poimirlem26  37901  poimirlem30  37905  poimir  37908  mblfinlem1  37912  ftc1anc  37956  heiborlem1  38066  lcvbr2  39402  lcvbr3  39403  cvrnbtwn  39651  cvrval2  39654  hlrelat2  39783  cdleme0nex  40670  aks4d1p7  42457  sticksstones1  42520  infdesc  43005  nna4b4nsq  43022  rencldnfilem  43181  setindtr  43385  onmaxnelsup  43584  onsupnmax  43589  onsupmaxb  43600  onsupeqnmax  43608  ordnexbtwnsuc  43628  gneispace  44494  iindif2f  45523  ralfal  45524  supxrgere  45696  supxrgelem  45700  infxrbnd2  45731  supminfxr  45826  limsupub  46066  limsuppnflem  46072  limsupre2lem  46086  stirlinglem5  46440  etransclem24  46620  etransclem32  46628  sge0iunmpt  46780  sge0rpcpnf  46783  iundjiun  46822  voliunsge0lem  46834  meaiuninc3v  46846  meaiininclem  46848  hoidmv1lelem3  46955  hoidmvlelem4  46960  hoidmvlelem5  46961  n0nsn2el  47389  0nelsetpreimafv  47754  stgr0  48324  gpg5nbgrvtx03starlem1  48432  gpg5nbgrvtx03starlem2  48433  gpg5nbgrvtx03starlem3  48434  gpg5nbgrvtx13starlem1  48435  gpg5nbgrvtx13starlem2  48436  gpg5nbgrvtx13starlem3  48437  gpg5edgnedg  48494  copisnmnd  48533  lindslinindsimp1  48821  lindslinindsimp2  48827  ldepslinc  48873  aacllem  50164