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

Theorem raleqbidv 2921
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 2913 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2725 . 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 1362   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710
This theorem is referenced by:  knatar  6035  ofrfval  6317  fmpt2x  6629  ovmptss  6643  marypha1lem  7671  supeq123d  7688  oieq1  7714  acneq  8201  isfin1a  8449  fpwwe2cbv  8784  fpwwe2lem2  8786  fpwwecbv  8798  fpwwelem  8799  eltskg  8904  elgrug  8946  cau3lem  12825  rlim  12956  ello1  12976  elo1  12987  caurcvg2  13138  caucvgb  13140  fsum2dlem  13220  fsumcom2  13224  pcfac  13943  vdwpc  14023  rami  14058  prdsval  14375  ismre  14510  isacs2  14573  acsfiel  14574  iscat  14592  iscatd  14593  catidex  14594  catideu  14595  cidfval  14596  cidval  14597  catlid  14603  catrid  14604  comfeq  14627  catpropd  14630  monfval  14653  issubc  14730  fullsubc  14742  isfunc  14756  funcpropd  14792  isfull  14802  isfth  14806  fthpropd  14813  natfval  14838  isposd  15107  lubfval  15130  glbfval  15143  ismnd  15399  grpidval  15414  ismndd  15426  mndpropd  15428  ismhm  15448  resmhm  15468  gsumvalx  15483  gsumpropd  15485  gsumress  15486  isgrp  15528  grppropd  15535  isgrpd2e  15539  isnsg  15689  nmznsg  15704  isghm  15726  isga  15788  subgga  15797  gsmsymgrfix  15912  gsmsymgreq  15916  gexval  16056  ispgp  16070  isslw  16086  sylow2blem2  16099  efgval  16193  efgi  16195  efgsdm  16206  cmnpropd  16265  iscmnd  16268  submcmn2  16302  gsumzaddlem  16387  gsumzaddlemOLD  16389  dmdprd  16453  dprdcntz  16465  isrng  16584  rngpropd  16611  isirred  16724  abvfval  16826  abvpropd  16850  islmod  16875  islmodd  16877  lmodprop2d  16930  lssset  16936  islmhm  17029  reslmhm  17054  lmhmpropd  17075  islbs  17078  rrgval  17279  isdomn  17287  isassa  17308  isassad  17315  assapropd  17319  ltbval  17484  opsrval  17487  psgndiflemA  17872  isphl  17898  islindf  18082  islindf2  18084  lsslindf  18100  istopg  18349  restbas  18603  ordtrest2  18649  cnfval  18678  cnpfval  18679  ist0  18765  ishaus  18767  iscnrm  18768  isnrm  18780  ist0-2  18789  ishaus2  18796  nrmsep3  18800  iscmp  18832  is1stc  18886  kgenval  18949  kgencn2  18971  txbas  18981  ptval  18984  dfac14  19032  isfil  19261  isufil  19317  isufl  19327  ucnval  19693  iscusp  19715  prdsxmslem2  19945  isnlm  20097  nmofval  20134  lebnumii  20379  iscau4  20631  iscmet  20636  iscmet3lem1  20643  iscmet3  20645  equivcmet  20667  ulmcaulem  21743  ulmcau  21744  fsumdvdscom  22409  dchrisumlem3  22624  pntibndlem2  22724  pntibnd  22726  pntlemp  22743  ostth2lem2  22767  istrkg2d  22806  trgcgrg  22847  iscusgra  23186  cusgrarn  23189  cusgra1v  23191  cusgra2v  23192  cusgra3v  23194  usgrasscusgra  23213  isuvtx  23218  uvtxel  23219  cusgrauvtxb  23226  iswlk  23248  istrl  23258  constr3trllem2  23359  isconngra  23380  isconngra1  23381  isplig  23486  gidval  23522  isgrp2d  23544  isgrpda  23606  isass  23625  isexid  23626  elghomlem1  23670  isrngo  23687  isrngod  23688  iscom2  23721  vci  23748  isvclem  23777  isnvlem  23810  lnoval  23974  ajfval  24031  isphg  24039  minvecolem3  24099  htth  24142  ressprs  25938  issrg  26041  isslmd  26066  resv1r  26158  ordtrest2NEW  26206  fmcncfil  26214  issiga  26407  isrnsigaOLD  26408  isrnsiga  26409  ismeas  26466  issibf  26566  sitgfval  26574  signstfvneq0  26820  ispcon  26959  isscon  26962  txpcon  26968  cvxpcon  26978  cvmscbv  26994  iscvm  26995  cvmsdisj  27006  cvmsss2  27010  snmlval  27067  fprod2dlem  27337  fprodcom2  27341  isptfin  28408  islocfin  28409  cover2g  28449  seqpo  28484  incsequz2  28486  caushft  28498  ismtyval  28540  rngohomval  28611  idlval  28654  pridlval  28674  maxidlval  28680  aomclem8  29256  islnm  29272  sdrgacs  29400  f12dfv  29989  f13dfv  29990  wlkelwrd  30123  iswwlk  30160  wlkiswwlk2  30174  wwlkn0s  30182  isclwwlk  30274  clwwlkprop  30276  clwlkisclwwlklem2  30291  isrgra  30386  isfrgra  30425  frgraunss  30430  frgra1v  30433  frgra2v  30434  frgra3v  30437  1vwmgra  30438  3vfriswmgra  30440  3cyclfrgrarn1  30447  n4cyclfrgra  30453  frgrancvvdeqlem4  30469  frgrawopreglem4  30483  frgrawopreg2  30487  frgraregorufr0  30488  islininds  30686  lindslinindsimp2  30703  ldepsnlinc  30756  lflset  32274  islfld  32277  isopos  32395  isoml  32453  isatl  32514  iscvlat  32538  ishlat1  32567  psubspset  32958  lautset  33296  pautsetN  33312  ldilfset  33322  ltrnfset  33331  dilfsetN  33366  trnfsetN  33369  trnsetN  33370  trlfset  33374  tendofset  33972  tendoset  33973  dihffval  34445  lpolsetN  34697  hdmapfval  35045  hgmapfval  35104
  Copyright terms: Public domain W3C validator