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

Theorem ralbidva 2893
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.)
Hypothesis
Ref Expression
ralbidva.1
Assertion
Ref Expression
ralbidva
Distinct variable group:   ,

Proof of Theorem ralbidva
StepHypRef Expression
1 ralbidva.1 . . 3
21pm5.74da 687 . 2
32ralbidv2 2892 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ralbidv  2896  2ralbidva  2899  raleqbidva  3070  ordunisssuc  4985  poinxp  5068  soinxp  5069  frinxp  5070  fnmptfvd  5990  funimass3  6003  fnnfpeq0  6102  fnsuppresOLD  6131  cocan1  6194  cocan2  6195  isores2  6229  isoini2  6235  ofrfval  6548  ofrfval2  6557  tfindsg2  6696  f1oweALT  6784  fnsuppres  6946  dfsmo2  7037  smores  7042  smores2  7044  ac6sfi  7784  fimaxg  7787  ordunifi  7790  isfinite2  7798  fipreima  7846  supisolem  7952  ordiso2  7961  ordtypelem7  7970  cantnf  8133  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  rankval3b  8265  rankonidlem  8267  iscard  8377  acndom  8453  dfac12lem3  8546  kmlem2  8552  cflim2  8664  cfsmolem  8671  ttukeylem6  8915  alephreg  8978  suplem2pr  9452  axsup  9681  sup3  10525  infm3  10527  suprleub  10532  dfinfmr  10545  infmrgelb  10548  ofsubeq0  10558  ofsubge0  10560  zextlt  10962  prime  10968  suprfinzcl  11003  indstr  11179  supxr2  11534  supxrbnd1  11542  supxrbnd2  11543  supxrleub  11547  supxrbnd  11549  infmxrgelb  11555  fzshftral  11795  mptnn0fsupp  12103  swrdeq  12671  swrdsymbeq  12672  clim  13317  rlim  13318  clim2  13327  clim2c  13328  clim0c  13330  ello1mpt  13344  lo1o1  13355  o1lo1  13360  climabs0  13408  o1compt  13410  rlimdiv  13468  geomulcvg  13685  mertenslem2  13694  mertens  13695  rpnnen2  13959  sqrt2irr  13982  pc11  14403  pcz  14404  1arith  14445  vdwlem8  14506  vdwlem11  14509  vdw  14512  ramval  14526  pwsle  14889  mrieqvd  15035  mreacs  15055  cidpropd  15105  ismon2  15129  monpropd  15132  isepi  15135  isepi2  15136  subsubc  15222  funcres2b  15266  funcpropd  15269  isfull2  15280  isfth2  15284  fucsect  15341  fucinv  15342  pospropd  15764  ipodrsfi  15793  tsrss  15853  grpidpropd  15888  mndpropd  15946  grppropd  16068  issubg4  16220  gass  16339  gsmsymgrfixlem1  16452  gsmsymgreqlem2  16456  gexdvds  16604  gexdvds2  16605  subgpgp  16617  sylow3lem6  16652  efgval2  16742  efgsp1  16755  dprdf11  17063  dprdf11OLD  17070  subgdmdprd  17081  ringpropd  17230  abvpropd  17491  lsspropd  17663  lbspropd  17745  assapropd  17976  psrbaglefi  18023  psrbaglefiOLD  18024  psrbagconf1o  18026  gsumbagdiaglem  18027  mplmonmul  18126  gsumply1eq  18347  phlpropd  18690  ishil2  18750  lindfmm  18862  islindf4  18873  islindf5  18874  scmatf1  19033  cpmatmcllem  19219  cpmatmcl  19220  decpmataa0  19269  decpmatmulsumfsupp  19274  pmatcollpw2lem  19278  pm2mpmhmlem1  19319  tgss2  19489  isclo  19588  neips  19614  opnnei  19621  isperf3  19654  ssidcn  19756  lmbrf  19761  cnnei  19783  cnrest2  19787  lmss  19799  lmres  19801  ist1-2  19848  ist1-3  19850  isreg2  19878  cmpfi  19908  bwth  19910  1stccn  19964  subislly  19982  kgencn  20057  ptclsg  20116  ptcnplem  20122  xkococnlem  20160  xkoinjcn  20188  tgqtop  20213  qtopcn  20215  fbflim  20477  flimrest  20484  flfnei  20492  isflf  20494  cnflf  20503  fclsopn  20515  fclsbas  20522  fclsrest  20525  isfcf  20535  cnfcf  20543  ptcmplem3  20554  tmdgsum2  20595  eltsms  20631  tsmsgsum  20637  tsmsgsumOLD  20640  tsmssubm  20644  tsmsf1o  20647  utopsnneiplem  20750  ismet2  20836  prdsxmetlem  20871  elmopn2  20948  prdsbl  20994  metss  21011  metrest  21027  metcnp  21044  metcnp2  21045  metcn  21046  metucnOLD  21091  metucn  21092  nrginvrcn  21200  metdsge  21353  divcn  21372  elcncf2  21394  mulc1cncf  21409  cncfmet  21412  evth2  21460  lmmbr2  21698  lmmbrf  21701  iscfil2  21705  cfil3i  21708  iscau2  21716  iscau4  21718  iscauf  21719  caucfil  21722  iscmet3lem3  21729  cfilres  21735  causs  21737  lmclim  21741  rrxmet  21835  evthicc2  21872  cniccbdd  21873  ovolfioo  21879  ovolficc  21880  ismbl2  21938  mbfsup  22071  mbfinf  22072  mbflimsup  22073  0plef  22079  mbfi1flim  22130  xrge0f  22138  itg2mulclem  22153  itgeqa  22220  ellimc2  22281  ellimc3  22283  limcflf  22285  cnlimc  22292  dvferm1  22386  dvferm2  22388  rolle  22391  dvivthlem1  22409  ftc1lem6  22442  itgsubst  22450  mdegle0  22477  deg1leb  22495  plydivex  22693  ulm2  22780  ulmcaulem  22789  ulmcau  22790  ulmdvlem3  22797  abelthlem9  22835  abelth  22836  rlimcnp  23295  ftalem3  23348  issqf  23410  sqf11  23413  dvdsmulf1o  23470  dchrelbas4  23518  dchrinv  23536  2sqlem6  23644  chpo1ubb  23666  dchrmusumlema  23678  dchrisum0lema  23699  ostth3  23823  eqeelen  24207  brbtwn2  24208  colinearalg  24213  axcgrid  24219  axsegconlem1  24220  ax5seglem4  24235  ax5seglem5  24236  axbtwnid  24242  axpasch  24244  axeuclidlem  24265  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem12  24278  wwlknext  24724  clwwlkel  24793  clwwlkf  24794  wwlkext2clwwlk  24803  wwlksubclwwlk  24804  clwlkfclwwlk  24844  extwwlkfablem2  25078  numclwwlkovf2ex  25086  isgrpo2  25199  nmounbi  25691  blocnilem  25719  isph  25737  phoeqi  25773  h2hcau  25896  h2hlm  25897  hial2eq2  26024  hoeq1  26749  hoeq2  26750  adjsym  26752  cnvadj  26811  hhcno  26823  hhcnf  26824  adjvalval  26856  leop2  27043  leoptri  27055  mdbr2  27215  dmdbr2  27222  mddmd2  27228  cdj3lem3b  27359  toslublem  27655  tosglblem  27657  submarchi  27730  isarchi3  27731  cmpcref  27853  lmdvg  27935  eulerpartlemd  28305  subfacp1lem3  28626  subfacp1lem5  28628  dfrdg2  29228  itg2gt0cn  30070  ftc1cnnc  30089  opnrebl  30138  lmclim2  30251  caures  30253  sstotbnd2  30270  rrnmet  30325  rrncmslem  30328  isdrngo3  30362  isidlc  30412  wepwsolem  30987  fnwe2lem2  30997  islnm2  31024  isprm7  31192  caofcan  31228  evthiccabs  31529  ellimcabssub0  31623  climf  31628  clim2f  31642  clim2cf  31656  clim0cf  31660  fourierdlem70  31959  fourierdlem71  31960  fourierdlem73  31962  fourierdlem80  31969  fourierdlem83  31972  fourierdlem87  31976  islinindfis  33050  aacllem  33216  cvrval2  34999  isat3  35032  iscvlat2N  35049  glbconN  35101  ltrneq  35873  cdlemefrs29clN  36125  cdlemefrs32fva  36126  cdleme32fva  36163  cdlemk33N  36635  cdlemk34  36636  cdlemkid3N  36659  cdlemkid4  36660  diaglbN  36782  dibglbN  36893  dihglbcpreN  37027  dihglblem6  37067  hdmap1eulem  37551  hdmap1eulemOLDN  37552  hdmapoc  37661  hlhilocv  37687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812
  Copyright terms: Public domain W3C validator