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

Theorem raleqbidv 3012
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 3004 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2838 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 261 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1454   A.wral 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753
This theorem is referenced by:  f12dfv  6196  f13dfv  6197  knatar  6272  ofrfval  6565  fmpt2x  6885  ovmptss  6903  marypha1lem  7972  supeq123d  7989  oieq1  8052  acneq  8499  isfin1a  8747  fpwwe2cbv  9080  fpwwe2lem2  9082  fpwwecbv  9094  fpwwelem  9095  eltskg  9200  elgrug  9242  cau3lem  13465  rlim  13607  ello1  13627  elo1  13638  caurcvg2  13792  caucvgb  13794  fsum2dlem  13879  fsumcom2  13883  fprod2dlem  14082  fprodcom2  14086  pcfac  14892  vdwpc  14978  rami  15020  prmgaplem7  15075  prdsval  15401  ismre  15544  isacs2  15607  acsfiel  15608  iscat  15626  iscatd  15627  catidex  15628  catideu  15629  cidfval  15630  cidval  15631  catlid  15637  catrid  15638  comfeq  15659  catpropd  15662  monfval  15685  issubc  15788  fullsubc  15803  isfunc  15817  funcpropd  15853  isfull  15863  isfth  15867  fthpropd  15874  natfval  15899  initoval  15940  termoval  15941  isposd  16249  lubfval  16272  glbfval  16285  ismgm  16537  grpidval  16551  gsumvalx  16561  gsumpropd  16563  gsumress  16567  issgrp  16576  ismnddef  16586  ismndOLD  16590  ismndd  16607  mndpropd  16610  ismhm  16632  resmhm  16654  isgrp  16725  grppropd  16732  isgrpd2e  16736  isnsg  16894  nmznsg  16909  isghm  16931  isga  16993  subgga  17002  gsmsymgrfix  17117  gsmsymgreq  17121  gexval  17275  gexvalOLD  17277  ispgp  17292  isslw  17308  sylow2blem2  17321  efgval  17415  efgi  17417  efgsdm  17428  cmnpropd  17487  iscmnd  17490  submcmn2  17527  gsumzaddlem  17602  dmdprd  17678  dprdcntz  17688  issrg  17789  isring  17832  ringpropd  17860  isirred  17975  abvfval  18094  abvpropd  18118  islmod  18143  islmodd  18145  lmodprop2d  18198  lssset  18205  islmhm  18298  reslmhm  18323  lmhmpropd  18344  islbs  18347  rrgval  18559  isdomn  18566  isassa  18587  isassad  18595  assapropd  18599  ltbval  18743  opsrval  18746  psgndiflemA  19217  isphl  19243  islindf  19418  islindf2  19420  lsslindf  19436  dmatval  19565  dmatcrng  19575  scmatcrng  19594  cpmat  19781  istopg  19973  restbas  20222  ordtrest2  20268  cnfval  20297  cnpfval  20298  ist0  20384  ishaus  20386  iscnrm  20387  isnrm  20399  ist0-2  20408  ishaus2  20415  nrmsep3  20419  iscmp  20451  is1stc  20504  isptfin  20579  islocfin  20580  kgenval  20598  kgencn2  20620  txbas  20630  ptval  20633  dfac14  20681  isfil  20910  isufil  20966  isufl  20976  flfcntr  21106  ucnval  21340  iscusp  21362  prdsxmslem2  21592  isnlm  21726  nmofval  21767  nmofvalOLD  21786  lebnumii  22045  iscau4  22297  iscmet  22302  iscmet3lem1  22309  iscmet3  22311  equivcmet  22333  ulmcaulem  23397  ulmcau  23398  fsumdvdscom  24162  dchrisumlem3  24377  pntibndlem2  24477  pntibnd  24479  pntlemp  24496  ostth2lem2  24520  trgcgrg  24608  tgcgr4  24624  isismt  24627  iscusgra  25232  cusgrarn  25235  cusgra1v  25237  cusgra2v  25238  cusgra3v  25240  usgrasscusgra  25259  isuvtx  25264  uvtxel  25265  cusgrauvtxb  25272  iswlk  25296  wlkelwrd  25306  istrl  25315  constr3trllem2  25427  isconngra  25448  isconngra1  25449  iswwlk  25459  wlkiswwlk2  25473  isclwwlk  25544  clwwlkprop  25546  clwlkisclwwlklem2  25562  isrgra  25702  isfrgra  25766  frgraunss  25771  frgra1v  25774  frgra2v  25775  frgra3v  25778  1vwmgra  25779  3vfriswmgra  25781  3cyclfrgrarn1  25788  n4cyclfrgra  25794  frgrancvvdeqlem4  25809  frgrawopreglem4  25823  frgrawopreg2  25827  frgraregorufr0  25828  isplig  25957  gidval  25989  isgrp2d  26011  isgrpda  26073  isass  26092  isexid  26093  elghomlem1OLD  26137  isrngo  26154  isrngod  26155  iscom2  26188  vci  26215  isvclem  26244  isnvlem  26277  lnoval  26441  ajfval  26498  isphg  26506  minvecolem3  26566  minvecolem3OLD  26576  htth  26619  ressprs  28464  isslmd  28566  resv1r  28648  iscref  28719  ordtrest2NEW  28777  fmcncfil  28785  issiga  28981  isrnsigaOLD  28982  isrnsiga  28983  isldsys  29026  ismeas  29069  carsgval  29183  issibf  29214  sitgfval  29222  signstfvneq0  29509  istrkg2d  29531  ispcon  29994  isscon  29997  txpcon  30003  cvxpcon  30013  cvmscbv  30029  iscvm  30030  cvmsdisj  30041  cvmsss2  30045  snmlval  30102  elmrsubrn  30206  ismfs  30235  mclsval  30249  fwddifnval  30978  poimirlem28  32012  cover2g  32085  seqpo  32120  incsequz2  32122  caushft  32134  ismtyval  32176  rngohomval  32247  idlval  32290  pridlval  32310  maxidlval  32316  lflset  32669  islfld  32672  isopos  32790  isoml  32848  isatl  32909  iscvlat  32933  ishlat1  32962  psubspset  33353  lautset  33691  pautsetN  33707  ldilfset  33717  ltrnfset  33726  dilfsetN  33762  trnfsetN  33765  trnsetN  33766  trlfset  33770  tendofset  34369  tendoset  34370  dihffval  34842  lpolsetN  35094  hdmapfval  35442  hgmapfval  35501  aomclem8  35963  islnm  35979  sdrgacs  36111  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem1OLD  37842  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  iccpartiltu  38773  iccelpart  38784  nbgr2vtx1edg  39467  nbuhgr2vtx1edgb  39469  uvtxaval  39508  uvtxael  39509  uvtxael1  39517  uvtxusgrel  39525  iscplgr  39531  cusgredg  39541  cplgr3v  39551  cplgrop  39553  usgredgsscusgredg  39569  isrgr  39626  isewlk  39668  is1wlk  39675  isWlk  39676  isconngr  39929  isconngr1  39930  1conngr  39934  mgmpropd  40047  ismgmd  40048  ismgmhm  40055  resmgmhm  40070  iscllaw  40097  iscomlaw  40098  isasslaw  40100  isrng  40148  c0snmgmhm  40186  zlidlring  40200  uzlidlring  40201  dmatALTval  40465  islininds  40511  lindslinindsimp2  40528  ldepsnlinc  40573  elbigo  40634
  Copyright terms: Public domain W3C validator