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

Theorem raleqbidv 3046
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 3038 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2871 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 256 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787
This theorem is referenced by:  f12dfv  6187  f13dfv  6188  knatar  6263  ofrfval  6553  fmpt2x  6873  ovmptss  6888  marypha1lem  7953  supeq123d  7970  oieq1  8027  acneq  8472  isfin1a  8720  fpwwe2cbv  9054  fpwwe2lem2  9056  fpwwecbv  9068  fpwwelem  9069  eltskg  9174  elgrug  9216  cau3lem  13396  rlim  13537  ello1  13557  elo1  13568  caurcvg2  13722  caucvgb  13724  fsum2dlem  13809  fsumcom2  13813  fprod2dlem  14012  fprodcom2  14016  pcfac  14798  vdwpc  14884  rami  14926  prmgaplem7  14981  prdsval  15303  ismre  15438  isacs2  15501  acsfiel  15502  iscat  15520  iscatd  15521  catidex  15522  catideu  15523  cidfval  15524  cidval  15525  catlid  15531  catrid  15532  comfeq  15553  catpropd  15556  monfval  15579  issubc  15682  fullsubc  15697  isfunc  15711  funcpropd  15747  isfull  15757  isfth  15761  fthpropd  15768  natfval  15793  initoval  15834  termoval  15835  isposd  16143  lubfval  16166  glbfval  16179  ismgm  16431  grpidval  16445  gsumvalx  16455  gsumpropd  16457  gsumress  16461  issgrp  16470  ismnddef  16480  ismndOLD  16484  ismndd  16501  mndpropd  16504  ismhm  16526  resmhm  16548  isgrp  16619  grppropd  16626  isgrpd2e  16630  isnsg  16788  nmznsg  16803  isghm  16825  isga  16887  subgga  16896  gsmsymgrfix  17011  gsmsymgreq  17015  gexval  17156  ispgp  17170  isslw  17186  sylow2blem2  17199  efgval  17293  efgi  17295  efgsdm  17306  cmnpropd  17365  iscmnd  17368  submcmn2  17405  gsumzaddlem  17480  dmdprd  17556  dprdcntz  17566  issrg  17667  isring  17710  ringpropd  17738  isirred  17853  abvfval  17972  abvpropd  17996  islmod  18021  islmodd  18023  lmodprop2d  18076  lssset  18083  islmhm  18176  reslmhm  18201  lmhmpropd  18222  islbs  18225  rrgval  18437  isdomn  18444  isassa  18465  isassad  18473  assapropd  18477  ltbval  18621  opsrval  18624  psgndiflemA  19091  isphl  19117  islindf  19292  islindf2  19294  lsslindf  19310  dmatval  19439  dmatcrng  19449  scmatcrng  19468  cpmat  19655  istopg  19847  restbas  20096  ordtrest2  20142  cnfval  20171  cnpfval  20172  ist0  20258  ishaus  20260  iscnrm  20261  isnrm  20273  ist0-2  20282  ishaus2  20289  nrmsep3  20293  iscmp  20325  is1stc  20378  isptfin  20453  islocfin  20454  kgenval  20472  kgencn2  20494  txbas  20504  ptval  20507  dfac14  20555  isfil  20784  isufil  20840  isufl  20850  flfcntr  20980  ucnval  21214  iscusp  21236  prdsxmslem2  21466  isnlm  21600  nmofval  21637  lebnumii  21881  iscau4  22133  iscmet  22138  iscmet3lem1  22145  iscmet3  22147  equivcmet  22169  ulmcaulem  23205  ulmcau  23206  fsumdvdscom  23968  dchrisumlem3  24183  pntibndlem2  24283  pntibnd  24285  pntlemp  24302  ostth2lem2  24326  trgcgrg  24413  isismt  24430  iscusgra  25020  cusgrarn  25023  cusgra1v  25025  cusgra2v  25026  cusgra3v  25028  usgrasscusgra  25047  isuvtx  25052  uvtxel  25053  cusgrauvtxb  25060  iswlk  25084  wlkelwrd  25094  istrl  25103  constr3trllem2  25215  isconngra  25236  isconngra1  25237  iswwlk  25247  wlkiswwlk2  25261  isclwwlk  25332  clwwlkprop  25334  clwlkisclwwlklem2  25350  isrgra  25490  isfrgra  25554  frgraunss  25559  frgra1v  25562  frgra2v  25563  frgra3v  25566  1vwmgra  25567  3vfriswmgra  25569  3cyclfrgrarn1  25576  n4cyclfrgra  25582  frgrancvvdeqlem4  25597  frgrawopreglem4  25611  frgrawopreg2  25615  frgraregorufr0  25616  isplig  25745  gidval  25777  isgrp2d  25799  isgrpda  25861  isass  25880  isexid  25881  elghomlem1OLD  25925  isrngo  25942  isrngod  25943  iscom2  25976  vci  26003  isvclem  26032  isnvlem  26065  lnoval  26229  ajfval  26286  isphg  26294  minvecolem3  26354  htth  26397  ressprs  28245  isslmd  28347  resv1r  28430  iscref  28501  ordtrest2NEW  28559  fmcncfil  28567  issiga  28763  isrnsigaOLD  28764  isrnsiga  28765  isldsys  28808  ismeas  28851  carsgval  28955  issibf  28985  sitgfval  28993  signstfvneq0  29240  istrkg2d  29262  ispcon  29725  isscon  29728  txpcon  29734  cvxpcon  29744  cvmscbv  29760  iscvm  29761  cvmsdisj  29772  cvmsss2  29776  snmlval  29833  elmrsubrn  29937  ismfs  29966  mclsval  29980  fwddifnval  30706  poimirlem28  31662  cover2g  31735  seqpo  31770  incsequz2  31772  caushft  31784  ismtyval  31826  rngohomval  31897  idlval  31940  pridlval  31960  maxidlval  31966  lflset  32324  islfld  32327  isopos  32445  isoml  32503  isatl  32564  iscvlat  32588  ishlat1  32617  psubspset  33008  lautset  33346  pautsetN  33362  ldilfset  33372  ltrnfset  33381  dilfsetN  33417  trnfsetN  33420  trnsetN  33421  trlfset  33425  tendofset  34024  tendoset  34025  dihffval  34497  lpolsetN  34749  hdmapfval  35097  hgmapfval  35156  aomclem8  35615  islnm  35631  sdrgacs  35756  ioodvbdlimc1lem1  37365  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  iccpartiltu  38116  iccelpart  38127  mgmpropd  38523  ismgmd  38524  ismgmhm  38531  resmgmhm  38546  iscllaw  38573  iscomlaw  38574  isasslaw  38576  isrng  38624  c0snmgmhm  38662  zlidlring  38676  uzlidlring  38677  dmatALTval  38943  islininds  38989  lindslinindsimp2  39006  ldepsnlinc  39051  elbigo  39113
  Copyright terms: Public domain W3C validator