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

Theorem raleqbidv 3068
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
Hypotheses
Ref Expression
raleqbidv.1
raleqbidv.2
Assertion
Ref Expression
raleqbidv
Distinct variable groups:   ,   ,   ,

Proof of Theorem raleqbidv
StepHypRef Expression
1 raleqbidv.1 . . 3
21raleqdv 3060 . 2
3 raleqbidv.2 . . 3
43ralbidv 2896 . 2
52, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  A.wral 2807
This theorem is referenced by:  f12dfv  6179  f13dfv  6180  knatar  6253  ofrfval  6548  fmpt2x  6866  ovmptss  6881  marypha1lem  7913  supeq123d  7930  oieq1  7958  acneq  8445  isfin1a  8693  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwecbv  9043  fpwwelem  9044  eltskg  9149  elgrug  9191  cau3lem  13187  rlim  13318  ello1  13338  elo1  13349  caurcvg2  13500  caucvgb  13502  fsum2dlem  13585  fsumcom2  13589  fprod2dlem  13784  fprodcom2  13788  pcfac  14418  vdwpc  14498  rami  14533  prdsval  14852  ismre  14987  isacs2  15050  acsfiel  15051  iscat  15069  iscatd  15070  catidex  15071  catideu  15072  cidfval  15073  cidval  15074  catlid  15080  catrid  15081  comfeq  15101  catpropd  15104  monfval  15127  issubc  15204  fullsubc  15219  isfunc  15233  funcpropd  15269  isfull  15279  isfth  15283  fthpropd  15290  natfval  15315  isposd  15585  lubfval  15608  glbfval  15621  ismgm  15873  grpidval  15887  gsumvalx  15897  gsumpropd  15899  gsumress  15903  issgrp  15912  ismnddef  15922  ismndOLD  15926  ismndd  15943  mndpropd  15946  ismhm  15968  resmhm  15990  isgrp  16061  grppropd  16068  isgrpd2e  16072  isnsg  16230  nmznsg  16245  isghm  16267  isga  16329  subgga  16338  gsmsymgrfix  16453  gsmsymgreq  16457  gexval  16598  ispgp  16612  isslw  16628  sylow2blem2  16641  efgval  16735  efgi  16737  efgsdm  16748  cmnpropd  16807  iscmnd  16810  submcmn2  16847  gsumzaddlem  16934  gsumzaddlemOLD  16936  dmdprd  17029  dprdcntz  17041  issrg  17159  isring  17202  ringpropd  17230  isirred  17348  abvfval  17467  abvpropd  17491  islmod  17516  islmodd  17518  lmodprop2d  17572  lssset  17580  islmhm  17673  reslmhm  17698  lmhmpropd  17719  islbs  17722  rrgval  17935  isdomn  17943  isassa  17964  isassad  17972  assapropd  17976  ltbval  18136  opsrval  18139  psgndiflemA  18637  isphl  18663  islindf  18847  islindf2  18849  lsslindf  18865  dmatval  18994  dmatcrng  19004  scmatcrng  19023  cpmat  19210  istopg  19404  restbas  19659  ordtrest2  19705  cnfval  19734  cnpfval  19735  ist0  19821  ishaus  19823  iscnrm  19824  isnrm  19836  ist0-2  19845  ishaus2  19852  nrmsep3  19856  iscmp  19888  is1stc  19942  isptfin  20017  islocfin  20018  kgenval  20036  kgencn2  20058  txbas  20068  ptval  20071  dfac14  20119  isfil  20348  isufil  20404  isufl  20414  ucnval  20780  iscusp  20802  prdsxmslem2  21032  isnlm  21184  nmofval  21221  lebnumii  21466  iscau4  21718  iscmet  21723  iscmet3lem1  21730  iscmet3  21732  equivcmet  21754  ulmcaulem  22789  ulmcau  22790  fsumdvdscom  23461  dchrisumlem3  23676  pntibndlem2  23776  pntibnd  23778  pntlemp  23795  ostth2lem2  23819  istrkg2d  23856  trgcgrg  23906  isismt  23921  iscusgra  24456  cusgrarn  24459  cusgra1v  24461  cusgra2v  24462  cusgra3v  24464  usgrasscusgra  24483  isuvtx  24488  uvtxel  24489  cusgrauvtxb  24496  iswlk  24520  wlkelwrd  24530  istrl  24539  constr3trllem2  24651  isconngra  24672  isconngra1  24673  iswwlk  24683  wlkiswwlk2  24697  isclwwlk  24768  clwwlkprop  24770  clwlkisclwwlklem2  24786  isrgra  24926  isfrgra  24990  frgraunss  24995  frgra1v  24998  frgra2v  24999  frgra3v  25002  1vwmgra  25003  3vfriswmgra  25005  3cyclfrgrarn1  25012  n4cyclfrgra  25018  frgrancvvdeqlem4  25033  frgrawopreglem4  25047  frgrawopreg2  25051  frgraregorufr0  25052  isplig  25179  gidval  25215  isgrp2d  25237  isgrpda  25299  isass  25318  isexid  25319  elghomlem1OLD  25363  isrngo  25380  isrngod  25381  iscom2  25414  vci  25441  isvclem  25470  isnvlem  25503  lnoval  25667  ajfval  25724  isphg  25732  minvecolem3  25792  htth  25835  ressprs  27643  isslmd  27745  resv1r  27827  iscref  27847  ordtrest2NEW  27905  fmcncfil  27913  issiga  28111  isrnsigaOLD  28112  isrnsiga  28113  ismeas  28170  issibf  28275  sitgfval  28283  signstfvneq0  28529  ispcon  28668  isscon  28671  txpcon  28677  cvxpcon  28687  cvmscbv  28703  iscvm  28704  cvmsdisj  28715  cvmsss2  28719  snmlval  28776  elmrsubrn  28880  ismfs  28909  mclsval  28923  cover2g  30205  seqpo  30240  incsequz2  30242  caushft  30254  ismtyval  30296  rngohomval  30367  idlval  30410  pridlval  30430  maxidlval  30436  aomclem8  31007  islnm  31023  sdrgacs  31150  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  mgmpropd  32463  ismgmd  32464  ismgmhm  32471  resmgmhm  32486  iscllaw  32513  iscomlaw  32514  isasslaw  32516  initoval  32603  termoval  32604  isrng  32682  c0snmgmhm  32720  zlidlring  32734  uzlidlring  32735  dmatALTval  33001  islininds  33047  lindslinindsimp2  33064  ldepsnlinc  33109  lflset  34784  islfld  34787  isopos  34905  isoml  34963  isatl  35024  iscvlat  35048  ishlat1  35077  psubspset  35468  lautset  35806  pautsetN  35822  ldilfset  35832  ltrnfset  35841  dilfsetN  35877  trnfsetN  35880  trnsetN  35881  trlfset  35885  tendofset  36484  tendoset  36485  dihffval  36957  lpolsetN  37209  hdmapfval  37557  hgmapfval  37616
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  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812
  Copyright terms: Public domain W3C validator