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

Theorem raleqbidv 2952
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 2944 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2756 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 253 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2741
This theorem is referenced by:  knatar  6069  ofrfval  6349  fmpt2x  6661  ovmptss  6675  marypha1lem  7704  supeq123d  7721  oieq1  7747  acneq  8234  isfin1a  8482  fpwwe2cbv  8818  fpwwe2lem2  8820  fpwwecbv  8832  fpwwelem  8833  eltskg  8938  elgrug  8980  cau3lem  12863  rlim  12994  ello1  13014  elo1  13025  caurcvg2  13176  caucvgb  13178  fsum2dlem  13258  fsumcom2  13262  pcfac  13982  vdwpc  14062  rami  14097  prdsval  14414  ismre  14549  isacs2  14612  acsfiel  14613  iscat  14631  iscatd  14632  catidex  14633  catideu  14634  cidfval  14635  cidval  14636  catlid  14642  catrid  14643  comfeq  14666  catpropd  14669  monfval  14692  issubc  14769  fullsubc  14781  isfunc  14795  funcpropd  14831  isfull  14841  isfth  14845  fthpropd  14852  natfval  14877  isposd  15146  lubfval  15169  glbfval  15182  ismnd  15438  grpidval  15453  ismndd  15465  mndpropd  15467  ismhm  15487  resmhm  15508  gsumvalx  15523  gsumpropd  15525  gsumress  15528  isgrp  15570  grppropd  15577  isgrpd2e  15581  isnsg  15731  nmznsg  15746  isghm  15768  isga  15830  subgga  15839  gsmsymgrfix  15954  gsmsymgreq  15958  gexval  16098  ispgp  16112  isslw  16128  sylow2blem2  16141  efgval  16235  efgi  16237  efgsdm  16248  cmnpropd  16307  iscmnd  16310  submcmn2  16344  gsumzaddlem  16429  gsumzaddlemOLD  16431  dmdprd  16502  dprdcntz  16514  issrg  16631  isrng  16671  rngpropd  16698  isirred  16813  abvfval  16925  abvpropd  16949  islmod  16974  islmodd  16976  lmodprop2d  17029  lssset  17037  islmhm  17130  reslmhm  17155  lmhmpropd  17176  islbs  17179  rrgval  17380  isdomn  17388  isassa  17409  isassad  17416  assapropd  17420  ltbval  17575  opsrval  17578  psgndiflemA  18053  isphl  18079  islindf  18263  islindf2  18265  lsslindf  18281  istopg  18530  restbas  18784  ordtrest2  18830  cnfval  18859  cnpfval  18860  ist0  18946  ishaus  18948  iscnrm  18949  isnrm  18961  ist0-2  18970  ishaus2  18977  nrmsep3  18981  iscmp  19013  is1stc  19067  kgenval  19130  kgencn2  19152  txbas  19162  ptval  19165  dfac14  19213  isfil  19442  isufil  19498  isufl  19508  ucnval  19874  iscusp  19896  prdsxmslem2  20126  isnlm  20278  nmofval  20315  lebnumii  20560  iscau4  20812  iscmet  20817  iscmet3lem1  20824  iscmet3  20826  equivcmet  20848  ulmcaulem  21881  ulmcau  21882  fsumdvdscom  22547  dchrisumlem3  22762  pntibndlem2  22862  pntibnd  22864  pntlemp  22881  ostth2lem2  22905  istrkg2d  22944  trgcgrg  22989  iscusgra  23386  cusgrarn  23389  cusgra1v  23391  cusgra2v  23392  cusgra3v  23394  usgrasscusgra  23413  isuvtx  23418  uvtxel  23419  cusgrauvtxb  23426  iswlk  23448  istrl  23458  constr3trllem2  23559  isconngra  23580  isconngra1  23581  isplig  23686  gidval  23722  isgrp2d  23744  isgrpda  23806  isass  23825  isexid  23826  elghomlem1  23870  isrngo  23887  isrngod  23888  iscom2  23921  vci  23948  isvclem  23977  isnvlem  24010  lnoval  24174  ajfval  24231  isphg  24239  minvecolem3  24299  htth  24342  ressprs  26138  isslmd  26240  resv1r  26327  ordtrest2NEW  26375  fmcncfil  26383  issiga  26576  isrnsigaOLD  26577  isrnsiga  26578  ismeas  26635  issibf  26741  sitgfval  26749  signstfvneq0  26995  ispcon  27134  isscon  27137  txpcon  27143  cvxpcon  27153  cvmscbv  27169  iscvm  27170  cvmsdisj  27181  cvmsss2  27185  snmlval  27242  fprod2dlem  27513  fprodcom2  27517  isptfin  28593  islocfin  28594  cover2g  28634  seqpo  28669  incsequz2  28671  caushft  28683  ismtyval  28725  rngohomval  28796  idlval  28839  pridlval  28859  maxidlval  28865  aomclem8  29440  islnm  29456  sdrgacs  29584  f12dfv  30172  f13dfv  30173  wlkelwrd  30306  iswwlk  30343  wlkiswwlk2  30357  wwlkn0s  30365  isclwwlk  30457  clwwlkprop  30459  clwlkisclwwlklem2  30474  isrgra  30569  isfrgra  30608  frgraunss  30613  frgra1v  30616  frgra2v  30617  frgra3v  30620  1vwmgra  30621  3vfriswmgra  30623  3cyclfrgrarn1  30630  n4cyclfrgra  30636  frgrancvvdeqlem4  30652  frgrawopreglem4  30666  frgrawopreg2  30670  frgraregorufr0  30671  dmatcrng  30920  scmatcrng  30927  islininds  30977  lindslinindsimp2  30994  ldepsnlinc  31047  cnstpmat  31061  lflset  32800  islfld  32803  isopos  32921  isoml  32979  isatl  33040  iscvlat  33064  ishlat1  33093  psubspset  33484  lautset  33822  pautsetN  33838  ldilfset  33848  ltrnfset  33857  dilfsetN  33892  trnfsetN  33895  trnsetN  33896  trlfset  33900  tendofset  34498  tendoset  34499  dihffval  34971  lpolsetN  35223  hdmapfval  35571  hgmapfval  35630
  Copyright terms: Public domain W3C validator