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

Theorem raleqbidv 2748
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 2742 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2563 . 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 1623   A.wral 2543
This theorem is referenced by:  knatar  5857  ofrfval  6086  fmpt2x  6190  ovmptss  6200  marypha1lem  7186  oieq1  7227  acneq  7670  isfin1a  7918  fpwwe2cbv  8252  fpwwe2lem2  8254  fpwwecbv  8266  fpwwelem  8267  eltskg  8372  elgrug  8414  cau3lem  11838  rlim  11969  ello1  11989  elo1  12000  caurcvg2  12150  caucvgb  12152  fsum2dlem  12233  fsumcom2  12237  pcfac  12947  vdwpc  13027  rami  13062  prdsval  13355  ismre  13492  isacs2  13555  acsfiel  13556  iscat  13574  iscatd  13575  catidex  13576  catideu  13577  cidfval  13578  cidval  13579  catidd  13582  catlid  13585  catrid  13586  comfeq  13609  catpropd  13612  monfval  13635  ismon  13636  issubc  13712  fullsubc  13724  isfunc  13738  funcpropd  13774  isfull  13784  isfth  13788  fthpropd  13795  natfval  13820  isposd  14089  lubfval  14112  glbfval  14117  islat  14153  spwval2  14333  isla  14342  ismnd  14369  grpidval  14384  ismndd  14396  mndpropd  14398  ismhm  14417  resmhm  14436  gsumvalx  14451  gsumpropd  14453  gsumress  14454  isgrp  14493  grppropd  14500  isgrpd2e  14504  isnsg  14646  nmznsg  14661  isghm  14683  isga  14745  subgga  14754  gexval  14889  ispgp  14903  isslw  14919  sylow2blem2  14932  efgval  15026  efgi  15028  efgsdm  15039  cmnpropd  15098  iscmnd  15101  submcmn2  15135  gsumzaddlem  15203  dmdprd  15236  dprdcntz  15243  isrng  15345  rngpropd  15372  isirred  15481  abvfval  15583  abvpropd  15607  islmod  15631  islmodd  15633  lmodprop2d  15687  lssset  15691  islmhm  15784  reslmhm  15809  lmhmpropd  15826  islbs  15829  rrgval  16028  isdomn  16035  isassa  16056  isassad  16063  assapropd  16067  ltbval  16213  opsrval  16216  isphl  16532  istopg  16641  restbas  16889  ordtrest2  16934  cnfval  16963  cnpfval  16964  ist0  17048  ishaus  17050  iscnrm  17051  isnrm  17063  ist0-2  17072  ishaus2  17079  nrmsep3  17083  iscmp  17115  is1stc  17167  kgenval  17230  kgencn2  17252  txbas  17262  ptval  17265  dfac14  17312  isfil  17542  isufil  17598  isufl  17608  prdsxmslem2  18075  isnlm  18186  nmofval  18223  lebnumii  18464  iscau4  18705  iscmet  18710  iscmet3lem1  18717  iscmet3  18719  equivcmet  18741  ulmcaulem  19771  ulmcau  19772  fsumdvdscom  20425  dchrisumlem3  20640  pntibndlem2  20740  pntibnd  20742  pntlemp  20759  ostth2lem2  20783  isplig  20844  gidval  20880  isgrp2d  20902  isgrpda  20964  isass  20983  isexid  20984  elghomlem1  21028  isrngo  21045  isrngod  21046  iscom2  21079  vci  21104  isvclem  21133  isnvlem  21166  lnoval  21330  ajfval  21387  isphg  21395  minvecolem3  21455  htth  21498  sigaval  23471  issiga  23472  isrnsigaOLD  23473  isrnsiga  23474  issgon  23484  ismeas  23530  ispcon  23754  isscon  23757  txpcon  23763  cvxpcon  23773  cvmscbv  23789  iscvm  23790  cvmsdisj  23801  cvmsss2  23805  snmlval  23914  isoriso  25212  mnlelt2  25266  mnlmxl2  25269  isdir2  25292  vecval1b  25451  vecval3b  25452  vri  25492  basexre  25522  istopx  25547  ismona  25809  isepia  25819  isfuna  25834  issrc  25867  propsrc  25868  isntr  25873  islimcat  25876  isnword  25986  indcls2  25996  pfsubkl  26047  pgapspf  26052  pgapspf2  26053  bisig0  26062  isibcg  26191  isptfin  26295  islocfin  26296  cover2g  26359  seqpo  26457  incsequz2  26459  caushft  26477  ismtyval  26524  rngohomval  26595  idlval  26638  pridlval  26658  maxidlval  26664  supeq123d  27158  aomclem8  27159  islnm  27175  islindf  27282  islindf2  27284  lsslindf  27300  sdrgacs  27509  iscusgra  28153  cusgra1v  28157  cusgra2v  28158  isuvtx  28160  uvtxel  28161  uvtxisvtx  28162  cusgrauvtx  28168  isfrgra  28171  frgra1v  28176  frgra3v  28180  1vwmgra  28181  3vfriswmgra  28183  lflset  29249  islfld  29252  isopos  29370  isoml  29428  isatl  29489  iscvlat  29513  ishlat1  29542  psubspset  29933  lautset  30271  pautsetN  30287  ldilfset  30297  ltrnfset  30306  dilfsetN  30341  trnfsetN  30344  trnsetN  30345  trlfset  30349  tendofset  30947  tendoset  30948  dihffval  31420  lpolsetN  31672  hdmapfval  32020  hgmapfval  32079
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator