MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralnex Unicode version

Theorem ralnex 2903
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
Assertion
Ref Expression
ralnex

Proof of Theorem ralnex
StepHypRef Expression
1 df-ral 2812 . 2
2 alinexa 1663 . . 3
3 df-rex 2813 . . 3
42, 3xchbinxr 311 . 2
51, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  e.wcel 1818  A.wral 2807  E.wrex 2808
This theorem is referenced by:  dfral2  2904  dfrex2  2908  ralinexa  2909  nrexralim  2911  nrex  2912  nrexdv  2913  r2exlem  2977  r19.43  3013  rabeq0  3807  iindif2  4399  rexiunxp  5148  rexxpf  5155  f0rn0  5775  ordunisuc2  6679  tfi  6688  omeulem1  7250  frfi  7785  isfinite2  7798  dfsup2OLD  7923  supmo  7932  ordtypelem9  7972  elirrv  8044  unbndrank  8281  kmlem7  8557  kmlem8  8558  kmlem13  8563  isfin1-3  8787  ac6num  8880  zorn2lem4  8900  fpwwe2lem12  9040  npomex  9395  genpnnp  9404  suplem2pr  9452  dedekind  9765  suprnub  10531  infmrgelb  10548  arch  10817  xrsupsslem  11527  xrinfmsslem  11528  supxrbnd1  11542  supxrbnd2  11543  supxrleub  11547  supxrbnd  11549  infmxrgelb  11555  injresinjlem  11925  hashgt12el  12481  hashgt12el2  12482  sqrt2irr  13982  prmind2  14228  vdwnnlem3  14515  vdwnn  14516  acsfiindd  15807  isnmnd  15924  isnirred  17349  lssne0  17597  bwth  19910  t1conperf  19937  trfbas  20345  fbunfip  20370  fbasrn  20385  filuni  20386  hausflim  20482  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem4  20555  lebnumlem3  21463  bcthlem4  21766  bcth3  21770  amgm  23320  issqf  23410  ostth  23824  tglowdim2ln  24032  axcontlem12  24278  usgranloop0  24380  vdusgra0nedg  24908  usgravd0nedg  24918  usgravd00  24919  nmounbi  25691  lnon0  25713  largei  27186  cvbr2  27202  chrelat2i  27284  uniinn0  27424  nn0min  27611  toslublem  27655  tosglblem  27657  archiabl  27742  lmdvg  27935  eulerpartlems  28299  dfon2lem8  29222  dfint3  29602  mblfinlem1  30051  ftc1anc  30098  heiborlem1  30307  rencldnfilem  30754  setindtr  30966  stirlinglem5  31860  etransclem24  32041  etransclem32  32049  copisnmnd  32497  lindslinindsimp1  33058  lindslinindsimp2  33064  ldepslinc  33110  aacllem  33216  bnj110  33916  bnj1417  34097  lcvbr2  34747  lcvbr3  34748  cvrnbtwn  34996  cvrval2  34999  hlrelat2  35127  cdleme0nex  36015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813
  Copyright terms: Public domain W3C validator