Theorem raleqbidv 3152

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

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 |- ( ph -> A = B )
2	1	raleqdv 3144	. 2 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	ralbidv 2986	. 2 |- ( ph -> ( A. x e. B ps <-> A. x e. B ch ) )
5	2, 4	bitrd 268	1 |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917

This theorem is referenced by:  f12dfv  6529  f13dfv  6530  knatar  6607  ofrfval  6905  fmpt2x  7236  ovmptss  7258  marypha1lem  8339  supeq123d  8356  oieq1  8417  acneq  8866  isfin1a  9114  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwecbv  9466  fpwwelem  9467  eltskg  9572  elgrug  9614  cau3lem  14094  rlim  14226  ello1  14246  elo1  14257  caurcvg2  14408  caucvgb  14410  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  pcfac  15603  vdwpc  15684  rami  15719  prmgaplem7  15761  prdsval  16115  ismre  16250  isacs2  16314  acsfiel  16315  iscat  16333  iscatd  16334  catidex  16335  catideu  16336  cidfval  16337  cidval  16338  catlid  16344  catrid  16345  comfeq  16366  catpropd  16369  monfval  16392  issubc  16495  fullsubc  16510  isfunc  16524  funcpropd  16560  isfull  16570  isfth  16574  fthpropd  16581  natfval  16606  initoval  16647  termoval  16648  isposd  16955  lubfval  16978  glbfval  16991  ismgm  17243  issstrmgm  17252  grpidval  17260  gsumvalx  17270  gsumpropd  17272  gsumress  17276  issgrp  17285  ismnddef  17296  ismndd  17313  mndpropd  17316  ismhm  17337  resmhm  17359  isgrp  17428  grppropd  17437  isgrpd2e  17441  isnsg  17623  nmznsg  17638  isghm  17660  isga  17724  subgga  17733  gsmsymgrfix  17848  gsmsymgreq  17852  gexval  17993  ispgp  18007  isslw  18023  sylow2blem2  18036  efgval  18130  efgi  18132  efgsdm  18143  cmnpropd  18202  iscmnd  18205  submcmn2  18244  gsumzaddlem  18321  dmdprd  18397  dprdcntz  18407  issrg  18507  isring  18551  ringpropd  18582  isirred  18699  abvfval  18818  abvpropd  18842  islmod  18867  islmodd  18869  lmodprop2d  18925  lssset  18934  islmhm  19027  reslmhm  19052  lmhmpropd  19073  islbs  19076  rrgval  19287  isdomn  19294  isassa  19315  isassad  19323  assapropd  19327  ltbval  19471  opsrval  19474  psgndiflemA  19947  isphl  19973  islindf  20151  islindf2  20153  lsslindf  20169  dmatval  20298  dmatcrng  20308  scmatcrng  20327  cpmat  20514  istopg  20700  restbas  20962  ordtrest2  21008  cnfval  21037  cnpfval  21038  ist0  21124  ishaus  21126  iscnrm  21127  isnrm  21139  ist0-2  21148  ishaus2  21155  nrmsep3  21159  iscmp  21191  is1stc  21244  isptfin  21319  islocfin  21320  kgenval  21338  kgencn2  21360  txbas  21370  ptval  21373  dfac14  21421  isfil  21651  isufil  21707  isufl  21717  flfcntr  21847  ucnval  22081  iscusp  22103  prdsxmslem2  22334  tngngp3  22460  isnlm  22479  nmofval  22518  lebnumii  22765  iscau4  23077  iscmet  23082  iscmet3lem1  23089  iscmet3  23091  equivcmet  23114  ulmcaulem  24148  ulmcau  24149  fsumdvdscom  24911  dchrisumlem3  25180  pntibndlem2  25280  pntibnd  25282  pntlemp  25299  ostth2lem2  25323  trgcgrg  25410  tgcgr4  25426  isismt  25429  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  uvtxaval  26287  uvtxael  26288  uvtxael1  26296  uvtxusgrel  26304  iscplgr  26310  cusgredg  26320  cplgr3v  26331  cplgrop  26333  usgredgsscusgredg  26355  isrgr  26455  isewlk  26498  iswlk  26506  iswwlks  26728  wlkiswwlks2  26761  isclwwlks  26880  clwlkclwwlklem1  26900  isconngr  27049  isconngr1  27050  1conngr  27054  isfrgr  27122  rspc2vd  27129  frgr1v  27135  nfrgr2v  27136  frgr3v  27139  1vwmgr  27140  3vfriswmgr  27142  3cyclfrgrrn1  27149  n4cyclfrgr  27155  isplig  27328  gidval  27366  vciOLD  27416  isvclem  27432  isnvlem  27465  lnoval  27607  ajfval  27664  isphg  27672  minvecolem3  27732  htth  27775  ressprs  29655  isslmd  29755  resv1r  29837  iscref  29911  ordtrest2NEW  29969  fmcncfil  29977  issiga  30174  isrnsigaOLD  30175  isrnsiga  30176  isldsys  30219  ismeas  30262  carsgval  30365  issibf  30395  sitgfval  30403  signstfvneq0  30649  istrkg2d  30744  ispconn  31205  issconn  31208  txpconn  31214  cvxpconn  31224  cvmscbv  31240  iscvm  31241  cvmsdisj  31252  cvmsss2  31256  snmlval  31313  elmrsubrn  31417  ismfs  31446  mclsval  31460  fwddifnval  32270  bj-ismoore  33059  poimirlem28  33437  cover2g  33509  seqpo  33543  incsequz2  33545  caushft  33557  ismtyval  33599  isass  33645  isexid  33646  elghomlem1OLD  33684  isrngo  33696  isrngod  33697  isgrpda  33754  rngohomval  33763  iscom2  33794  idlval  33812  pridlval  33832  maxidlval  33838  lflset  34346  islfld  34349  isopos  34467  isoml  34525  isatl  34586  iscvlat  34610  ishlat1  34639  psubspset  35030  lautset  35368  pautsetN  35384  ldilfset  35394  ltrnfset  35403  dilfsetN  35439  trnfsetN  35442  trnsetN  35443  trlfset  35447  tendofset  36046  tendoset  36047  dihffval  36519  lpolsetN  36771  hdmapfval  37119  hgmapfval  37178  aomclem8  37631  islnm  37647  sdrgacs  37771  clsk1independent  38344  gneispace2  38430  gneispaceel2  38442  gneispacess2  38444  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  issal  40534  isome  40708  iccpartiltu  41358  iccelpart  41369  isupwlk  41717  mgmpropd  41775  ismgmd  41776  ismgmhm  41783  resmgmhm  41798  iscllaw  41825  iscomlaw  41826  isasslaw  41828  isrng  41876  c0snmgmhm  41914  zlidlring  41928  uzlidlring  41929  dmatALTval  42189  islininds  42235  lindslinindsimp2  42252  ldepsnlinc  42297  elbigo  42345