Theorem ralnex 2992

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	|- ( A. x e. A -. ph <-> -. E. x e. A ph )

Proof of Theorem ralnex

Step	Hyp	Ref	Expression
1		raln 2991	. 2 |- ( A. x e. A -. ph <-> A. x -. ( x e. A /\ ph ) )
2		alnex 1706	. . 3 |- ( A. x -. ( x e. A /\ ph ) <-> -. E. x ( x e. A /\ ph ) )
3		df-rex 2918	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
4	2, 3	xchbinxr 325	. 2 |- ( A. x -. ( x e. A /\ ph ) <-> -. E. x e. A ph )
5	1, 4	bitri 264	1 |- ( A. x e. A -. ph <-> -. E. x e. A ph )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  dfral2  2994  dfrex2  2996  ralinexa  2997  nrexralim  2999  nrex  3000  nrexdv  3001  r19.43  3093  rabeq0OLD  3960  n0snor2el  4364  iindif2  4589  rexiunxp  5262  rexxpf  5269  f0rn0  6090  ordunisuc2  7044  tfi  7053  omeulem1  7662  frfi  8205  isfinite2  8218  supmo  8358  infmo  8401  ordtypelem9  8431  elirrv  8504  unbndrank  8705  kmlem7  8978  kmlem8  8979  kmlem13  8984  isfin1-3  9208  ac6num  9301  zorn2lem4  9321  fpwwe2lem12  9463  npomex  9818  genpnnp  9827  suplem2pr  9875  dedekind  10200  suprnub  10988  infregelb  11007  arch  11289  xrsupsslem  12137  xrinfmsslem  12138  supxrbnd1  12151  supxrbnd2  12152  supxrleub  12156  supxrbnd  12158  infxrgelb  12165  injresinjlem  12588  hashgt12el  13210  hashgt12el2  13211  sqrt2irr  14979  prmind2  15398  vdwnnlem3  15701  vdwnn  15702  acsfiindd  17177  isnmnd  17298  isnirred  18700  lssne0  18951  bwth  21213  t1connperf  21239  trfbas  21648  fbunfip  21673  fbasrn  21688  filuni  21689  hausflim  21785  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem4  21859  lebnumlem3  22762  bcthlem4  23124  bcth3  23128  amgm  24717  issqf  24862  ostth  25328  tglowdim2ln  25546  axcontlem12  25855  umgrnloop0  26004  numedglnl  26039  usgrnloop0ALT  26097  uhgrnbgr0nb  26250  nbgr0edg  26253  vtxd0nedgb  26384  vtxdusgr0edgnelALT  26392  1hevtxdg0  26401  usgrvd0nedg  26429  uhgrvd00  26430  pthdlem2lem  26663  nmounbi  27631  lnon0  27653  largei  29126  cvbr2  29142  chrelat2i  29224  uniinn0  29366  infxrge0gelb  29531  nn0min  29567  toslublem  29667  tosglblem  29669  archiabl  29752  lmdvg  29999  esumcvgre  30153  eulerpartlems  30422  bnj110  30928  bnj1417  31109  dfon2lem8  31695  nosupbnd1lem4  31857  sltrec  31924  dfint3  32059  unblimceq0  32498  relowlpssretop  33212  poimirlem26  33435  poimirlem30  33439  poimir  33442  mblfinlem1  33446  ftc1anc  33493  heiborlem1  33610  lcvbr2  34309  lcvbr3  34310  cvrnbtwn  34558  cvrval2  34561  hlrelat2  34689  cdleme0nex  35577  rencldnfilem  37384  setindtr  37591  gneispace  38432  nelrnmpt  39257  supxrgere  39549  supxrgelem  39553  infxrbnd2  39585  supminfxr  39694  limsupub  39936  limsuppnflem  39942  limsupre2lem  39956  stirlinglem5  40295  etransclem24  40475  etransclem32  40483  sge0iunmpt  40635  sge0rpcpnf  40638  iundjiun  40677  voliunsge0lem  40689  meaiininclem  40700  hoidmv1lelem3  40807  hoidmvlelem4  40812  hoidmvlelem5  40813  copisnmnd  41809  lindslinindsimp1  42246  lindslinindsimp2  42252  ldepslinc  42298  aacllem  42547