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

Theorem raleqbidv 2908
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
Hypotheses
Ref Expression
raleqbidv.1  |-  ( ph  ->  A  =  B )
raleqbidv.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
raleqbidv  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Distinct variable groups:    x, A    x, B    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem raleqbidv
StepHypRef Expression
1 raleqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
21raleqdv 2902 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2717 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 245 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   A.wral 2697
This theorem is referenced by:  knatar  6072  ofrfval  6305  fmpt2x  6409  ovmptss  6420  marypha1lem  7430  supeq123d  7447  oieq1  7473  acneq  7916  isfin1a  8164  fpwwe2cbv  8497  fpwwe2lem2  8499  fpwwecbv  8511  fpwwelem  8512  eltskg  8617  elgrug  8659  cau3lem  12150  rlim  12281  ello1  12301  elo1  12312  caurcvg2  12463  caucvgb  12465  fsum2dlem  12546  fsumcom2  12550  pcfac  13260  vdwpc  13340  rami  13375  prdsval  13670  ismre  13807  isacs2  13870  acsfiel  13871  iscat  13889  iscatd  13890  catidex  13891  catideu  13892  cidfval  13893  cidval  13894  catlid  13900  catrid  13901  comfeq  13924  catpropd  13927  monfval  13950  issubc  14027  fullsubc  14039  isfunc  14053  funcpropd  14089  isfull  14099  isfth  14103  fthpropd  14110  natfval  14135  isposd  14404  lubfval  14427  glbfval  14432  islat  14468  spwval2  14648  isla  14657  ismnd  14684  grpidval  14699  ismndd  14711  mndpropd  14713  ismhm  14732  resmhm  14751  gsumvalx  14766  gsumpropd  14768  gsumress  14769  isgrp  14808  grppropd  14815  isgrpd2e  14819  isnsg  14961  nmznsg  14976  isghm  14998  isga  15060  subgga  15069  gexval  15204  ispgp  15218  isslw  15234  sylow2blem2  15247  efgval  15341  efgi  15343  efgsdm  15354  cmnpropd  15413  iscmnd  15416  submcmn2  15450  gsumzaddlem  15518  dmdprd  15551  dprdcntz  15558  isrng  15660  rngpropd  15687  isirred  15796  abvfval  15898  abvpropd  15922  islmod  15946  islmodd  15948  lmodprop2d  15998  lssset  16002  islmhm  16095  reslmhm  16120  lmhmpropd  16137  islbs  16140  rrgval  16339  isdomn  16346  isassa  16367  isassad  16374  assapropd  16378  ltbval  16524  opsrval  16527  isphl  16851  istopg  16960  restbas  17214  ordtrest2  17260  cnfval  17289  cnpfval  17290  ist0  17376  ishaus  17378  iscnrm  17379  isnrm  17391  ist0-2  17400  ishaus2  17407  nrmsep3  17411  iscmp  17443  is1stc  17496  kgenval  17559  kgencn2  17581  txbas  17591  ptval  17594  dfac14  17642  isfil  17871  isufil  17927  isufl  17937  ucnval  18299  iscusp  18321  prdsxmslem2  18551  isnlm  18703  nmofval  18740  lebnumii  18983  iscau4  19224  iscmet  19229  iscmet3lem1  19236  iscmet3  19238  equivcmet  19260  ulmcaulem  20302  ulmcau  20303  fsumdvdscom  20962  dchrisumlem3  21177  pntibndlem2  21277  pntibnd  21279  pntlemp  21296  ostth2lem2  21320  iscusgra  21457  cusgrarn  21460  cusgra1v  21462  cusgra2v  21463  cusgra3v  21465  usgrasscusgra  21484  isuvtx  21489  uvtxel  21490  cusgrauvtxb  21497  iswlk  21519  istrl  21529  constr3trllem2  21630  isconngra  21651  isconngra1  21652  isplig  21757  gidval  21793  isgrp2d  21815  isgrpda  21877  isass  21896  isexid  21897  elghomlem1  21941  isrngo  21958  isrngod  21959  iscom2  21992  vci  22019  isvclem  22048  isnvlem  22081  lnoval  22245  ajfval  22302  isphg  22310  minvecolem3  22370  htth  22413  fmcncfil  24309  issiga  24486  isrnsigaOLD  24487  isrnsiga  24488  ismeas  24545  issibf  24640  sitgfval  24647  ispcon  24902  isscon  24905  txpcon  24911  cvxpcon  24921  cvmscbv  24937  iscvm  24938  cvmsdisj  24949  cvmsss2  24953  snmlval  25010  fprod2dlem  25296  fprodcom2  25300  isptfin  26366  islocfin  26367  cover2g  26407  seqpo  26442  incsequz2  26444  caushft  26458  ismtyval  26500  rngohomval  26571  idlval  26614  pridlval  26634  maxidlval  26640  aomclem8  27127  islnm  27143  islindf  27250  islindf2  27252  lsslindf  27268  sdrgacs  27477  f12dfv  28066  f13dfv  28067  isfrgra  28317  frgraunss  28322  frgra1v  28325  frgra3v  28329  1vwmgra  28330  3vfriswmgra  28332  3cyclfrgrarn1  28339  n4cyclfrgra  28345  frgrancvvdeqlem4  28359  frgrawopreglem4  28373  frgrawopreg2  28377  frgraregorufr0  28378  lflset  29794  islfld  29797  isopos  29915  isoml  29973  isatl  30034  iscvlat  30058  ishlat1  30087  psubspset  30478  lautset  30816  pautsetN  30832  ldilfset  30842  ltrnfset  30851  dilfsetN  30886  trnfsetN  30889  trnsetN  30890  trlfset  30894  tendofset  31492  tendoset  31493  dihffval  31965  lpolsetN  32217  hdmapfval  32565  hgmapfval  32624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
  Copyright terms: Public domain W3C validator