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

Theorem raleqbidv 2761
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 2755 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2576 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 244 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   A.wral 2556
This theorem is referenced by:  knatar  5873  ofrfval  6102  fmpt2x  6206  ovmptss  6216  marypha1lem  7202  oieq1  7243  acneq  7686  isfin1a  7934  fpwwe2cbv  8268  fpwwe2lem2  8270  fpwwecbv  8282  fpwwelem  8283  eltskg  8388  elgrug  8430  cau3lem  11854  rlim  11985  ello1  12005  elo1  12016  caurcvg2  12166  caucvgb  12168  fsum2dlem  12249  fsumcom2  12253  pcfac  12963  vdwpc  13043  rami  13078  prdsval  13371  ismre  13508  isacs2  13571  acsfiel  13572  iscat  13590  iscatd  13591  catidex  13592  catideu  13593  cidfval  13594  cidval  13595  catidd  13598  catlid  13601  catrid  13602  comfeq  13625  catpropd  13628  monfval  13651  ismon  13652  issubc  13728  fullsubc  13740  isfunc  13754  funcpropd  13790  isfull  13800  isfth  13804  fthpropd  13811  natfval  13836  isposd  14105  lubfval  14128  glbfval  14133  islat  14169  spwval2  14349  isla  14358  ismnd  14385  grpidval  14400  ismndd  14412  mndpropd  14414  ismhm  14433  resmhm  14452  gsumvalx  14467  gsumpropd  14469  gsumress  14470  isgrp  14509  grppropd  14516  isgrpd2e  14520  isnsg  14662  nmznsg  14677  isghm  14699  isga  14761  subgga  14770  gexval  14905  ispgp  14919  isslw  14935  sylow2blem2  14948  efgval  15042  efgi  15044  efgsdm  15055  cmnpropd  15114  iscmnd  15117  submcmn2  15151  gsumzaddlem  15219  dmdprd  15252  dprdcntz  15259  isrng  15361  rngpropd  15388  isirred  15497  abvfval  15599  abvpropd  15623  islmod  15647  islmodd  15649  lmodprop2d  15703  lssset  15707  islmhm  15800  reslmhm  15825  lmhmpropd  15842  islbs  15845  rrgval  16044  isdomn  16051  isassa  16072  isassad  16079  assapropd  16083  ltbval  16229  opsrval  16232  isphl  16548  istopg  16657  restbas  16905  ordtrest2  16950  cnfval  16979  cnpfval  16980  ist0  17064  ishaus  17066  iscnrm  17067  isnrm  17079  ist0-2  17088  ishaus2  17095  nrmsep3  17099  iscmp  17131  is1stc  17183  kgenval  17246  kgencn2  17268  txbas  17278  ptval  17281  dfac14  17328  isfil  17558  isufil  17614  isufl  17624  prdsxmslem2  18091  isnlm  18202  nmofval  18239  lebnumii  18480  iscau4  18721  iscmet  18726  iscmet3lem1  18733  iscmet3  18735  equivcmet  18757  ulmcaulem  19787  ulmcau  19788  fsumdvdscom  20441  dchrisumlem3  20656  pntibndlem2  20756  pntibnd  20758  pntlemp  20775  ostth2lem2  20799  isplig  20860  gidval  20896  isgrp2d  20918  isgrpda  20980  isass  20999  isexid  21000  elghomlem1  21044  isrngo  21061  isrngod  21062  iscom2  21095  vci  21120  isvclem  21149  isnvlem  21182  lnoval  21346  ajfval  21403  isphg  21411  minvecolem3  21471  htth  21514  sigaval  23486  issiga  23487  isrnsigaOLD  23488  isrnsiga  23489  issgon  23499  ismeas  23545  ispcon  23769  isscon  23772  txpcon  23778  cvxpcon  23788  cvmscbv  23804  iscvm  23805  cvmsdisj  23816  cvmsss2  23820  snmlval  23929  isoriso  25315  mnlelt2  25369  mnlmxl2  25372  isdir2  25395  vecval1b  25554  vecval3b  25555  vri  25595  basexre  25625  istopx  25650  ismona  25912  isepia  25922  isfuna  25937  issrc  25970  propsrc  25971  isntr  25976  islimcat  25979  isnword  26089  indcls2  26099  pfsubkl  26150  pgapspf  26155  pgapspf2  26156  bisig0  26165  isibcg  26294  isptfin  26398  islocfin  26399  cover2g  26462  seqpo  26560  incsequz2  26562  caushft  26580  ismtyval  26627  rngohomval  26698  idlval  26741  pridlval  26761  maxidlval  26767  supeq123d  27261  aomclem8  27262  islnm  27278  islindf  27385  islindf2  27387  lsslindf  27403  sdrgacs  27612  iscusgra  28292  cusgra1v  28296  cusgra2v  28297  cusgra3v  28299  isuvtx  28301  uvtxel  28302  uvtxisvtx  28303  cusgrauvtx  28309  iswlk  28329  istrl  28336  constr3trllem2  28397  isfrgra  28417  frgra1v  28422  frgra3v  28426  1vwmgra  28427  3vfriswmgra  28429  3cyclfrgrarn1  28435  n4cyclfrgra  28440  lflset  29871  islfld  29874  isopos  29992  isoml  30050  isatl  30111  iscvlat  30135  ishlat1  30164  psubspset  30555  lautset  30893  pautsetN  30909  ldilfset  30919  ltrnfset  30928  dilfsetN  30963  trnfsetN  30966  trnsetN  30967  trlfset  30971  tendofset  31569  tendoset  31570  dihffval  32042  lpolsetN  32294  hdmapfval  32642  hgmapfval  32701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator