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  3213  cbvrexdva  3218  cbvrexfw  3279  rexeqbidvvOLD  3310  cbvrexdva2  3322  rexeqf  3330  rexprg  4661  n0snor2el  4797  iindif2  5041  rexiunxp  5804  rexxpf  5811  f0rn0  6745  ordunisuc2  7820  tfi  7829  resf1extb  7910  releldmdifi  8024  omeulem1  8546  frfi  9232  isfinite2  9245  supmo  9403  infmo  9448  ordtypelem9  9479  elirrv  9549  unbndrank  9795  kmlem7  10110  kmlem8  10111  kmlem13  10116  isfin1-3  10339  ac6num  10432  zorn2lem4  10452  fpwwe2lem11  10594  npomex  10949  suplem2pr  11006  dedekind  11337  suprnub  12148  infregelb  12167  arch  12439  xrsupsslem  13267  xrinfmsslem  13268  supxrbnd1  13281  supxrbnd2  13282  supxrleub  13286  supxrbnd  13288  infxrgelb  13296  injresinjlem  13748  hashgt12el  14387  hashgt12el2  14388  sqrt2irr  16217  prmind2  16655  vdwnnlem3  16968  vdwnn  16969  acsfiindd  18512  isnmnd  18665  isnirred  20329  lssne0  20857  bwth  23297  t1connperf  23323  trfbas  23731  fbunfip  23756  fbasrn  23771  filuni  23772  hausflim  23868  alexsubALTlem3  23936  alexsubALTlem4  23937  ptcmplem4  23942  lebnumlem3  24862  bcthlem4  25227  bcth3  25231  amgm  26901  issqf  27046  ostth  27550  nosupbnd1lem4  27623  noinfbnd1lem4  27638  sltrec  27732  cuteq1  27746  tglowdim2ln  28578  axcontlem12  28902  umgrnloop0  29036  numedglnl  29071  usgrnloop0ALT  29132  uhgrnbgr0nb  29281  nbgr0edg  29284  vtxd0nedgb  29416  vtxdusgr0edgnelALT  29424  1hevtxdg0  29433  usgrvd0nedg  29461  uhgrvd00  29462  pthdlem2lem  29697  nmounbi  30705  lnon0  30727  largei  32196  cvbr2  32212  chrelat2i  32294  n0nsnel  32444  uniinn0  32479  infxrge0gelb  32689  nn0min  32745  toslublem  32898  tosglblem  32900  archiabl  33152  lmdvg  33943  esumcvgre  34081  eulerpartlems  34351  bnj110  34848  bnj1417  35031  lfuhgr3  35107  fmlaomn0  35377  fmla0disjsuc  35385  fmlasucdisj  35386  dfon2lem8  35778  dfint3  35940  relowlpssretop  37352  domalom  37392  fvineqsneq  37400  poimirlem26  37640  poimirlem30  37644  poimir  37647  mblfinlem1  37651  ftc1anc  37695  heiborlem1  37805  lcvbr2  39015  lcvbr3  39016  cvrnbtwn  39264  cvrval2  39267  hlrelat2  39397  cdleme0nex  40284  aks4d1p7  42071  sticksstones1  42134  infdesc  42631  nna4b4nsq  42648  rencldnfilem  42808  setindtr  43013  onmaxnelsup  43212  onsupnmax  43217  onsupmaxb  43228  onsupeqnmax  43236  ordnexbtwnsuc  43256  gneispace  44123  nelrnmpt  45078  iindif2f  45154  ralfal  45155  supxrgere  45329  supxrgelem  45333  infxrbnd2  45365  supminfxr  45460  limsupub  45702  limsuppnflem  45708  limsupre2lem  45722  stirlinglem5  46076  etransclem24  46256  etransclem32  46264  sge0iunmpt  46416  sge0rpcpnf  46419  iundjiun  46458  voliunsge0lem  46470  meaiuninc3v  46482  meaiininclem  46484  hoidmv1lelem3  46591  hoidmvlelem4  46596  hoidmvlelem5  46597  n0nsn2el  47026  0nelsetpreimafv  47391  stgr0  47959  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  copisnmnd  48157  lindslinindsimp1  48446  lindslinindsimp2  48452  ldepslinc  48498  aacllem  49790