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

Theorem ralbidv 2896
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
Hypothesis
Ref Expression
ralbidv.1
Assertion
Ref Expression
ralbidv
Distinct variable group:   ,

Proof of Theorem ralbidv
StepHypRef Expression
1 ralbidv.1 . . 3
21adantr 465 . 2
32ralbidva 2893 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  A.wral 2807
This theorem is referenced by:  2ralbidv  2901  ralbiiOLD  2971  rexralbidv  2976  raleqbi1dv  3062  raleqbidv  3068  cbvral2v  3092  rspc2  3218  rspc3v  3222  reu6i  3290  reu7  3294  sbcralt  3408  raaan  3937  raaanv  3938  2ralsng  4066  r19.12snOLD  4096  2ralunsn  4238  elintg  4294  elintrabg  4299  eliin  4336  disjprg  4448  disjxun  4450  reusv2lem2  4654  reusv3  4660  reusv6OLD  4663  poeq1  4808  somo  4839  frirr  4861  fr2nr  4862  frminex  4864  wereu2  4881  posn  5073  frsn  5075  ralxpf  5154  cnvpo  5550  fnmptfvd  5990  iinpreima  6017  dff4  6045  dff13f  6167  eusvobj2  6289  ofreq  6543  sorpssuni  6589  sorpssint  6590  fr3nr  6615  onssmin  6632  funcnvuni  6753  f1oweALT  6784  frxp  6910  smoeq  7040  recseq  7062  tfrlem12  7077  tz7.48lem  7125  elixp2  7493  undifixp  7525  xpf1o  7699  nneneq  7720  ac6sfi  7784  frfi  7785  fipreima  7846  indexfi  7848  marypha1lem  7913  marypha1  7914  supeq1  7925  supeq3  7929  supmo  7932  eqsup  7936  supub  7939  suplub  7940  supmaxlemOLD  7945  supisoex  7953  oieq1  7958  ordtypecbv  7963  ordtypelem3  7966  ordtypelem6  7969  ordtypelem7  7970  ordtypelem9  7972  wemaplem1  7992  wemaplem2  7993  zfregcl  8041  oemapval  8123  oemapvali  8124  cantnf  8133  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  rankval3b  8265  unbndrank  8281  rankunb  8289  rankuni2b  8292  tcrank  8323  scottex  8324  scottexs  8326  scott0s  8327  bnd2  8332  dfac8clem  8434  ac5num  8438  acni  8447  acni2  8448  alephval3  8512  dfac4  8524  dfac5lem5  8529  dfac5  8530  dfac2a  8531  dfac2  8532  dfacacn  8542  kmlem2  8552  kmlem13  8563  cflem  8647  cflecard  8654  cfeq0  8657  cfsuc  8658  cfflb  8660  cofsmo  8670  cfsmolem  8671  cfcoflem  8673  coftr  8674  alephsing  8677  fin23lem11  8718  isfin3ds  8730  fin23lem17  8739  fin23lem39  8751  isf33lem  8767  isf34lem6  8781  fin1a2lem13  8813  hsmexlem4  8830  hsmex  8833  axcc2lem  8837  axcc3  8839  dcomex  8848  axdc2lem  8849  axdc3lem2  8852  axdc3lem3  8853  axdc3  8855  axdc4lem  8856  axcclem  8858  zorn2lem2  8898  zorn2lem7  8903  zorn2g  8904  zornn0g  8906  ttukeylem7  8916  axdclem2  8921  brdom3  8927  brdom7disj  8930  brdom6disj  8931  alephval2  8968  inar1  9174  axgroth6  9227  pinq  9326  nqereu  9328  prlem934  9432  supexpr  9453  supsrlem  9509  axpre-sup  9567  dedekind  9765  dedekindle  9766  fimaxre2  10516  lbreu  10518  sup2  10524  infm3  10527  supmul1  10533  supmullem2  10535  supmul  10536  infmrcl  10547  nnsub  10599  uzwo  11173  uzwoOLD  11174  nnwof  11177  uzinfmi  11190  ublbneg  11195  lbzbi  11199  zsupss  11200  uzsupss  11203  uzwo3  11206  zmax  11208  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem4  11240  rpnnen1lem5  11241  xrsupsslem  11527  xrinfmsslem  11528  xrsupss  11529  xrinfmss  11530  iccsupr  11646  supicc  11697  supiccub  11698  supicclub  11699  flval2  11950  flval3  11951  fsequb  12085  axdc4uzlem  12092  ssnn0fi  12094  fsuppmapnn0fiubex  12098  faclbnd4lem4  12374  bccl  12400  hashgt12el  12481  hashbc  12502  hashge2el2dif  12521  wrdind  12702  wrd2ind  12703  sqrlem3  13078  rexanre  13179  rexico  13186  cau4  13189  caubnd2  13190  caubnd  13191  clim  13317  rlim  13318  rlim2  13319  rlim2lt  13320  rlim3  13321  clim2  13327  clim2c  13328  clim0c  13330  rlim0  13331  rlim0lt  13332  ello12r  13340  ello1d  13346  lo1bdd2  13347  lo1bddrp  13348  elo12r  13351  rlimconst  13367  rlimresb  13388  rlimcld2  13401  climabs0  13408  rlimcn2  13413  reccn2  13419  cn1lem  13420  rlimo1  13439  o1rlimmul  13441  lo1add  13449  lo1mul  13450  isercoll  13490  caucvgrlem  13495  incexclem  13648  climcnds  13663  divrcnv  13664  ruclem12  13974  sqrt2irr  13982  gcdcllem1  14149  gcdcllem2  14150  maxprmfct  14254  reumodprminv  14329  pc2dvds  14402  pcz  14404  prmpwdvds  14422  infpn2  14431  prmreclem1  14434  prmreclem2  14435  prmreclem3  14436  prmreclem5  14438  prmreclem6  14439  vdwlem6  14504  vdwlem8  14506  vdwlem13  14511  vdwnnlem1  14513  vdwnn  14516  ramz  14543  ramcl  14547  cshwrepswhash1  14587  prdsleval  14874  imasval  14908  imasaddfnlem  14925  imasvscafn  14934  mrisval  15027  isacs  15048  isacs2  15050  isacs1i  15054  mreacs  15055  acsfn  15056  acsfn2  15060  iscatd  15070  catidex  15071  catideu  15072  cidval  15074  catidd  15077  comfeq  15101  catpropd  15104  ismon  15128  isfunc  15233  isnat  15316  isprs  15559  drsdirfi  15567  ispos  15576  lubfval  15608  lubeldm  15611  lubval  15614  lubprop  15616  lublecllem  15618  glbfval  15621  glbeldm  15624  glbval  15627  glbprop  15629  joinval2lem  15638  joinlem  15641  meetval2lem  15652  meetlem  15655  isglbd  15747  lubl  15750  lubun  15753  clatleglb  15756  poslubmo  15776  posglbmo  15777  poslubd  15778  ipodrsima  15795  isdlat  15823  mgm1  15884  mgmidmo  15886  ismgmid  15891  ismgmid2  15894  mgmidsssn0  15896  gsumvalx  15897  gsumress  15903  gsumval2  15907  sgrp1  15918  mndclOLD  15931  mndassOLD  15932  ismndd  15943  mnd1  15961  mnd1OLD  15962  mhmima  15994  mrcmndind  15997  gsumvallem2  16003  gsumwspan  16014  sgrp2rid2  16044  sgrp2rid2ex  16045  sgrp2nmndlem4  16046  isgrpinv  16100  mhmmnd  16192  issubg4  16220  0subg  16226  cycsubgcl  16227  isnsg2  16231  nsgacs  16237  elnmz  16240  ghmrn  16280  ghmnsgima  16290  isga  16329  orbsta  16351  cntzfval  16358  elcntz  16360  resscntz  16369  oppgsubg  16398  symgextfo  16447  gsmsymgreqlem2  16456  gsmsymgreq  16457  pmtrdifel  16505  pmtrdifwrdellem3  16508  pmtrdifwrdel2  16511  psgnunilem2  16520  psgnunilem3  16521  odeq  16574  gexid  16601  gexlem2  16602  gexdvds  16604  isslw  16628  pgpssslw  16634  sylow2alem1  16637  sylow2alem2  16638  efgval  16735  efgrelexlemb  16768  efgcpbllemb  16773  gexex  16859  abl1  16872  dmdprd  17029  dprd2da  17091  pgpfac1lem5  17130  ring1  17248  isabv  17468  islss  17581  lssacs  17613  reslmhm  17698  islbs  17722  pj1lmhm  17746  lbsacsbs  17802  isrrg  17936  opsrval  18139  ply1coe  18337  cply1coe0bi  18342  zringlpir  18512  zlpir  18517  psgndiflemA  18637  ocvfval  18697  elocv  18699  iunocv  18712  frlmlbs  18831  islindf  18847  islinds2  18848  islindf2  18849  lindfrn  18856  lsslindf  18865  islindf4  18873  mat0dimcrng  18972  mdetunilem1  19114  mdetunilem9  19122  cpmat  19210  cpmatel  19212  1elcpmat  19216  m2cpminvid2lem  19255  chfacffsupp  19357  chfacfscmulfsupp  19360  chfacfpmmulfsupp  19364  basgen2  19491  bastop1  19495  isclo  19588  ordtbaslem  19689  iscn  19736  cnpval  19737  iscnp  19738  iscnp3  19745  lmbr  19759  lmbr2  19760  lmbrf  19761  cnprest  19790  cnprest2  19791  t0sep  19825  isreg  19833  t1sep2  19870  tgcmp  19901  1stcclb  19945  1stcfb  19946  2ndc1stc  19952  1stcrest  19954  2ndcdisj  19957  islly  19969  isnlly  19970  lly1stc  19997  isref  20010  islocfin  20018  elkgen  20037  kgencn  20057  elpt  20073  elptr  20074  ptcnplem  20122  tx1stc  20151  cnmpt21  20172  kqt0lem  20237  isr0  20238  regr1lem2  20241  r0sep  20249  nrmr0reg  20250  flffbas  20496  cnflf  20503  cnflf2  20504  lmflf  20506  txflf  20507  fclsopni  20516  fclsnei  20520  fclsrest  20525  fcfnei  20536  cnfcf  20543  alexsubb  20546  alexsubALTlem3  20549  qustgplem  20619  tsmsfbas  20626  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  tsmsxplem1  20655  tsmsxp  20657  ustval  20705  isust  20706  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ust0  20722  utopval  20735  ucnval  20780  isucn  20781  isucn2  20782  ucnima  20784  iscfilu  20791  ispsmet  20808  ismet  20826  isxmet  20827  imasdsf1olem  20876  imasf1oxmet  20878  imasf1omet  20879  metss  21011  met1stc  21024  prdsxmslem2  21032  metcnpi3  21049  txmetcnp  21050  metucnOLD  21091  metucn  21092  nlmvscn  21196  nrginvrcnlem  21199  nmoval  21222  nmolb  21224  nghmcn  21252  qtopbaslem  21265  icccmplem2  21328  icccmplem3  21329  reconnlem2  21332  metdscn  21360  cncfval  21392  elcncf2  21394  elcncf1di  21399  mulc1cncf  21409  cncfmet  21412  cnllycmp  21456  evth  21459  lebnumlem3  21463  lebnum  21464  xlebnum  21465  ishtpy  21472  isphtpy  21481  pi1xfr  21555  pi1coghm  21561  ipcn  21686  lmmbr2  21698  lmmbr3  21699  lmmbrf  21701  cfilfval  21703  iscfil  21704  fmcfil  21711  caufval  21714  iscau  21715  iscau2  21716  iscau3  21717  iscau4  21718  iscauf  21719  caucfil  21722  cfilresi  21734  causs  21737  lmclim  21741  cncmet  21761  cmetcusp1OLD  21791  cmetcusp1  21792  minveclem4c  21840  minveclem2  21841  minveclem3b  21843  minveclem4  21847  minveclem6  21849  minveclem7  21850  ivthlem2  21864  ivthlem3  21865  cniccbdd  21873  ovolunlem1  21908  ovoliunlem1  21913  ovoliun2  21917  ovolicc2lem3  21930  ismbl  21937  ioombl1lem4  21971  uniioombllem2  21992  uniioombllem6  21997  dyadmax  22007  dyadmbllem  22008  dyadmbl  22009  opnmbllem  22010  volcn  22015  ismbf1  22033  ismbf  22037  mbfeqalem  22049  mbfinf  22072  mbflimsup  22073  itg1climres  22121  mbfi1fseqlem6  22127  mbfi1flimlem  22129  itg2seq  22149  itg2monolem1  22157  itg2i1fseq  22162  itg2i1fseq2  22163  itg2cnlem1  22168  itg2cnlem2  22169  isibl  22172  dveflem  22380  ply1divex  22537  fta1g  22568  plyeq0lem  22607  dgrco  22672  plydivex  22693  fta1  22704  vieta1  22708  aannenlem1  22724  aannenlem2  22725  aalioulem2  22729  aalioulem3  22730  ulmval  22775  ulm2  22780  ulmi  22781  ulmres  22783  ulmshftlem  22784  ulmcaulem  22789  ulmcau  22790  ulmss  22792  ulmbdd  22793  ulmdvlem1  22795  ulmdvlem3  22797  mtestbdd  22800  iblulm  22802  abelthlem8  22834  pilem2  22847  pilem3  22848  divlogrlim  23016  cxpcn3  23122  dmarea  23287  rlimcnp  23295  cxplim  23301  cxploglim  23307  scvxcvx  23315  emcllem6  23330  ftalem1  23346  ftalem2  23347  ftalem3  23348  isppw2  23389  perfectlem2  23505  2sqlem6  23644  2sqlem10  23649  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  dchrisum0  23705  pntpbnd  23773  pntibndlem3  23777  pntibnd  23778  pntleme  23793  pntlem3  23794  pntlemp  23795  pnt3  23797  istrkgld  23857  axtg5seg  23862  perpln1  24087  perpln2  24088  isperp  24089  brbtwn2  24208  colinearalg  24213  axsegconlem1  24220  axsegcon  24230  ax5seglem4  24235  ax5seglem5  24236  axlowdim  24264  axeuclidlem  24265  axcontlem1  24267  axcontlem2  24268  axcontlem4  24270  axcontlem5  24271  axcontlem8  24274  axcontlem12  24278  cusgra3v  24464  wlks  24519  wlkcompim  24526  wlkelwrd  24530  wlkntrllem3  24563  constr3trllem2  24651  1conngra  24675  wwlk  24681  clwwlk  24766  isrgrac  24934  rusgra0edg  24955  iseupa  24965  frgrawopreg1  25050  frgrawopreg2  25051  frgrareg  25117  frgraregord013  25118  isgrpo  25198  isgrpo2  25199  isgrpoi  25200  grpoideu  25211  grpoidinv2  25220  isgrp2d  25237  isgrpda  25299  exidu1  25328  cmpidelt  25331  cnid  25353  mulid  25358  ghgrpOLD  25370  isrngod  25381  rngoideu  25386  cnrngo  25405  vci  25441  isvclem  25470  isnvlem  25503  nvi  25507  nmcvcn  25605  lnoval  25667  islno  25668  isblo3i  25716  blo3i  25717  blocnilem  25719  blocni  25720  ajfval  25724  ubthlem1  25786  ubthlem2  25787  ubthlem3  25788  ubth  25789  minvecolem2  25791  minvecolem3  25792  minvecolem4c  25795  minvecolem4  25796  minvecolem5  25797  minvecolem6  25798  minvecolem7  25799  htthlem  25834  h2hcau  25896  h2hlm  25897  hilid  26078  hcau  26101  hlimi  26105  hlim2  26109  ocel  26199  adjsym  26752  ellnop  26777  ellnfn  26802  hhcno  26823  hhcnf  26824  0cnop  26898  0cnfn  26899  idcnop  26900  lnopeq  26928  elunop2  26932  lnophm  26938  lnconi  26952  lnopcnbd  26955  lnfncnbd  26976  imaelshi  26977  riesz3i  26981  riesz4i  26982  riesz4  26983  riesz1  26984  cnlnadjlem2  26987  cnlnadjlem5  26990  cnlnadjlem8  26993  cnlnadji  26995  nmopadjlei  27007  cnvbraval  27029  leopg  27041  leoppos  27045  mdbr  27213  dmdbr  27218  cdj3i  27360  rmoeq  27386  disjunsn  27453  funcnv5mpt  27511  fgreu  27513  fcnvgreu  27514  xrge0infss  27580  resspos  27647  isomnd  27691  inftmrel  27724  isinftm  27725  archiabl  27742  rngurd  27778  isarchiofld  27807  crefeq  27848  rge0scvg  27931  qqhcn  27972  esumpcvgval  28084  sigaval  28110  issgon  28123  isrnmeas  28171  ismbfm  28223  isanmbfm  28227  mbfmcst  28230  sitgval  28274  oddpwdc  28293  eulerpartlemd  28305  ballotleme  28435  signsw0g  28513  signswmnd  28514  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem5  28575  lgambdd  28579  lgamcvglem  28582  derangenlem  28615  subfacp1lem3  28626  subfacp1lem5  28628  subfacp1lem6  28629  subfacp1  28630  erdszelem8  28642  kur14  28660  cnpcon  28675  rescon  28691  cvmscbv  28703  iscvm  28704  cvmsi  28710  cvmsval  28711  cvmlift3lem2  28765  snmlval  28776  mclsssvlem  28922  mclsval  28923  mclsax  28929  mclsind  28930  ghomgrpilem1  29025  dfpo2  29184  dfon2lem9  29223  dfrdg2  29228  dfrdg3  29229  poseq  29333  soseq  29334  wrecseq123  29337  wfrlem1  29343  wfrlem15  29357  frrlem1  29387  sltval  29407  nocvxminlem  29450  nobndlem2  29453  nobndlem8  29459  nobndup  29460  nobnddown  29461  fin2so  30040  supaddc  30041  supadd  30042  heicant  30049  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  ismblfin  30055  voliunnfl  30058  volsupnfl  30059  mbfresfi  30061  itg2addnc  30069  ftc1anc  30098  nn0prpwlem  30140  isfne  30157  isfne4  30158  isfne2  30160  isfne3  30161  neibastop3  30180  topmeet  30182  topjoin  30183  filnetlem4  30199  f1opr  30215  upixp  30220  indexdom  30225  filbcmb  30231  sdclem2  30235  fdc  30238  lmclim2  30251  caures  30253  istotbnd  30265  istotbnd3  30267  sstotbnd  30271  isbnd  30276  heibor  30317  bfp  30320  rrncmslem  30328  exidres  30340  exidresid  30341  idlval  30410  isidl  30411  0idl  30422  unichnidl  30428  pridl  30434  ismaxidl  30437  smprngopr  30449  igenval2  30463  prnc  30464  ispridlc  30467  scottexf  30576  scott0f  30577  isnacs  30636  isnacs2  30638  nacsfix  30644  mzpclval  30657  elmzpcl  30658  rencldnfilem  30754  infmrgelbi  30814  pellfundre  30817  pellfundlb  30820  wepwsolem  30987  fnwe2lem2  30997  aomclem8  31007  dfac11  31008  gicabl  31047  islnr3  31064  hbtlem2  31073  hbtlem5  31077  evth2f  31390  ubelsupr  31395  evthf  31402  fnchoice  31404  dstregt0  31463  upbdrech2  31508  mccl  31606  mullimc  31622  ellimcabssub0  31623  limcdm0  31624  climf  31628  mullimcf  31629  constlimc  31630  idlimc  31632  clim2f  31642  limsupre  31647  limcleqr  31650  addlimc  31654  0ellimcdiv  31655  clim2cf  31656  clim0cf  31660  cncfshift  31676  cncfperiod  31681  fperdvper  31715  dvdivbd  31720  dvbdfbdioo  31727  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem3  31745  stoweidlem5  31787  stoweidlem9  31791  stoweidlem15  31797  stoweidlem16  31798  stoweidlem27  31809  stoweidlem28  31810  stoweidlem31  31813  stoweidlem34  31816  stoweidlem37  31819  stoweidlem46  31828  stoweidlem48  31830  stoweidlem51  31833  stoweidlem52  31834  stoweidlem59  31841  wallispilem3  31849  stirlinglem13  31868  fourierdlem2  31891  fourierdlem3  31892  fourierdlem16  31905  fourierdlem20  31909  fourierdlem21  31910  fourierdlem22  31911  fourierdlem25  31914  fourierdlem39  31928  fourierdlem42  31931  fourierdlem54  31943  fourierdlem64  31953  fourierdlem77  31966  fourierdlem83  31972  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  cbvral2  32177  raaan2  32180  2reu4a  32194  dfdfat2  32216  mgmhmima  32490  isinito  32606  istermo  32607  rnghmval  32697  lidlmsgrp  32732  lidlrng  32733  zlidlring  32734  uzlidlring  32735  2zrngamnd  32747  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  linindslinci  33049  lindslinindsimp1  33058  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  linds0  33066  lindsrng01  33069  snlindsntor  33072  lmod1  33093  ldepsnlinc  33109  bnj1185  33852  bnj1385  33891  bnj66  33918  bnj106  33926  bnj155  33937  bnj852  33979  bnj893  33986  bnj1228  34067  bnj1234  34069  bnj1463  34111  riotasvd  34687  islfl  34785  eqlkr  34824  eqlkr3  34826  glbconN  35101  hlsuprexch  35105  ispsubsp  35469  ldilset  35833  isldil  35834  dilsetN  35878  isdilN  35879  trlset  35886  trlval  35887  cdleme27b  36094  cdleme29b  36101  cdleme31so  36105  cdleme31sn1  36107  cdleme31sn1c  36114  cdleme31fv  36116  cdleme40v  36195  istendo  36486  cdlemkid3N  36659  cdlemkid4  36660  cdlemkid5  36661  dihfval  36958  dihval  36959  islpolN  37210  hdmapffval  37556  hdmapfval  37557  hdmapval  37558  hdmapval2lem  37561  hgmapffval  37615  hgmapfval  37616  hgmapval  37617  hgmapvs  37621  taupilemrplb  37695  fiinfi  37758  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37993
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