Theorem ralnex 3063

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 3060	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1783	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3062	. . 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 3051  ∃wrex 3061

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 3052  df-rex 3062

This theorem is referenced by:  dfrex2  3064  nrex  3065  rexim  3078  dfral2  3088  ralinexa  3090  r19.43  3105  ralnex2  3117  ralnex3  3118  nrexralim  3121  nrexdv  3132  nelb  3213  cbvrexdva  3218  cbvrexfw  3278  cbvrexdva2  3314  rexeqf  3319  rexprg  4641  n0snor2el  4776  iindif2  5019  rexiunxp  5795  rexxpf  5802  nelrnmpt  5922  f0rn0  6725  ordunisuc2  7795  tfi  7804  resf1extb  7885  releldmdifi  7998  omeulem1  8517  frfi  9195  isfinite2  9208  supmo  9365  infmo  9410  ordtypelem9  9441  elirrvOLD  9513  unbndrank  9766  kmlem7  10079  kmlem8  10080  kmlem13  10085  isfin1-3  10308  ac6num  10401  zorn2lem4  10421  fpwwe2lem11  10564  npomex  10919  suplem2pr  10976  dedekind  11309  suprnub  12121  infregelb  12140  arch  12434  xrsupsslem  13259  xrinfmsslem  13260  supxrbnd1  13273  supxrbnd2  13274  supxrleub  13278  supxrbnd  13280  infxrgelb  13288  injresinjlem  13745  hashgt12el  14384  hashgt12el2  14385  sqrt2irr  16216  prmind2  16654  vdwnnlem3  16968  vdwnn  16969  acsfiindd  18519  isnmnd  18706  isnirred  20400  lssne0  20946  bwth  23375  t1connperf  23401  trfbas  23809  fbunfip  23834  fbasrn  23849  filuni  23850  hausflim  23946  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem4  24020  lebnumlem3  24930  bcthlem4  25294  bcth3  25298  amgm  26954  issqf  27099  ostth  27602  nosupbnd1lem4  27675  noinfbnd1lem4  27690  ltsrec  27793  cuteq1  27809  tglowdim2ln  28719  axcontlem12  29044  umgrnloop0  29178  numedglnl  29213  usgrnloop0ALT  29274  uhgrnbgr0nb  29423  nbgr0edg  29426  vtxd0nedgb  29557  vtxdusgr0edgnelALT  29565  1hevtxdg0  29574  usgrvd0nedg  29602  uhgrvd00  29603  pthdlem2lem  29835  nmounbi  30847  lnon0  30869  largei  32338  cvbr2  32354  chrelat2i  32436  n0nsnel  32585  uniinn0  32620  infxrge0gelb  32839  nn0min  32894  toslublem  33032  tosglblem  33034  archiabl  33259  lmdvg  34097  esumcvgre  34235  eulerpartlems  34504  bnj110  35000  bnj1417  35183  fineqvnttrclselem1  35265  lfuhgr3  35302  fmlaomn0  35572  fmla0disjsuc  35580  fmlasucdisj  35581  dfon2lem8  35970  dfint3  36134  bj-axseprep  37381  relowlpssretop  37680  domalom  37720  fvineqsneq  37728  poimirlem26  37967  poimirlem30  37971  poimir  37974  mblfinlem1  37978  ftc1anc  38022  heiborlem1  38132  lcvbr2  39468  lcvbr3  39469  cvrnbtwn  39717  cvrval2  39720  hlrelat2  39849  cdleme0nex  40736  aks4d1p7  42522  sticksstones1  42585  infdesc  43076  nna4b4nsq  43093  rencldnfilem  43248  setindtr  43452  onmaxnelsup  43651  onsupnmax  43656  onsupmaxb  43667  onsupeqnmax  43675  ordnexbtwnsuc  43695  gneispace  44561  iindif2f  45590  ralfal  45591  supxrgere  45763  supxrgelem  45767  infxrbnd2  45798  supminfxr  45892  limsupub  46132  limsuppnflem  46138  limsupre2lem  46152  stirlinglem5  46506  etransclem24  46686  etransclem32  46694  sge0iunmpt  46846  sge0rpcpnf  46849  iundjiun  46888  voliunsge0lem  46900  meaiuninc3v  46912  meaiininclem  46914  hoidmv1lelem3  47021  hoidmvlelem4  47026  hoidmvlelem5  47027  n0nsn2el  47473  0nelsetpreimafv  47850  nprmmul1  47987  stgr0  48436  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5edgnedg  48606  copisnmnd  48645  lindslinindsimp1  48933  lindslinindsimp2  48939  ldepslinc  48985  aacllem  50276