Theorem raleqdv 3144

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)

Hypothesis

Ref	Expression
raleq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
raleqdv	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hints:   ph( x)   ps( x)

Proof of Theorem raleqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 |- ( ph -> A = B )
2		raleq 3138	. 2 |- ( A = B -> ( A. x e. A ps <-> A. x e. B ps ) )
3	1, 2	syl 17	1 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )

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:  raleqbidv  3152  raleqbidva  3154  raleleqALT  3157  raldifeq  4059  wfisg  5715  fveqressseq  6355  f12dfv  6529  f13dfv  6530  cbvfo  6544  isoselem  6591  ofrfval  6905  omsinds  7084  wfrlem4  7418  issmo2  7446  smoeq  7447  frfi  8205  marypha1lem  8339  marypha1  8340  dfoi  8416  oieq2  8418  ordtypecbv  8422  ordtypelem2  8424  ordtypelem3  8425  ordtypelem9  8431  wemapwe  8594  tcrank  8747  isacn  8867  pwsdompw  9026  isfin2  9116  isfin3ds  9151  isf33lem  9188  hsmexlem4  9251  zorn2lem6  9323  zorn2lem7  9324  zorn2g  9325  fpwwe2lem13  9464  uzsupss  11780  fzrevral2  12426  fzrevral3  12427  fzshftral  12428  fzoshftral  12585  uzsinds  12786  expmulnbnd  12996  eqs1  13392  swrdeq  13444  swrdspsleq  13449  2swrdeqwrdeq  13453  repswsymballbi  13527  cshw1  13568  wwlktovf1  13700  eqwrds3  13704  rexuz3  14088  rexuzre  14092  limsupgle  14208  rlim  14226  climconst  14274  rlimclim1  14276  climshftlem  14305  isercoll  14398  caucvgb  14410  serf0  14411  mertenslem1  14616  coprmprod  15375  coprmproddvds  15377  prmind2  15398  vdwlem10  15694  vdwlem13  15697  vdwnnlem2  15700  vdwnnlem3  15701  vdwnn  15702  ramval  15712  ramz  15729  prmgaplem5  15759  isacs  16312  cidpropd  16370  monpropd  16397  isssc  16480  fullsubc  16510  funcpropd  16560  isfth  16574  fthpropd  16581  grpidpropd  17261  mndpropd  17316  nmznsg  17638  ghmnsgima  17684  symgextfo  17842  gsmsymgrfixlem1  17847  gsmsymgrfix  17848  fvcosymgeq  17849  gsmsymgreqlem2  17851  symgfixf1  17857  psgnunilem3  17916  subgpgp  18012  sylow2blem3  18037  sylow3lem6  18047  efgsp1  18150  efgsres  18151  cmnpropd  18202  telgsumfzs  18386  ablfac2  18488  ringpropd  18582  abvpropd  18842  lsspropd  19017  lmhmpropd  19073  lbspropd  19099  pj1lmhm  19100  assapropd  19327  znf1o  19900  psgndiflemB  19946  phlpropd  20000  islindf  20151  lindfmm  20166  islindf4  20177  islindf5  20178  scmatf1  20337  isclo  20891  perfopn  20989  lmfval  21036  lmconst  21065  cncnp  21084  iscnrm2  21142  ist0-2  21148  ist1-2  21151  ishaus2  21155  ordtt1  21183  subislly  21284  elpt  21375  elptr  21376  ptbasfi  21384  tx1stc  21453  xkococnlem  21462  fclscmp  21834  ufilcmp  21836  cnpfcf  21845  alexsubALTlem1  21851  alexsubALTlem2  21852  alexsubALTlem4  21854  tmdgsum2  21900  tsmsf1o  21948  ustval  22006  ucnval  22081  imasdsf1olem  22178  imasf1oxmet  22180  imasf1omet  22181  metss  22313  prdsxmslem2  22334  cnmpt2pc  22727  lebnumlem3  22762  ishtpy  22771  pi1coghm  22861  lmnn  23061  evthicc  23228  cniccbdd  23230  ovolicc2lem4  23288  0pledm  23440  cniccibl  23607  c1lip1  23760  dvivthlem1  23771  lhop1  23777  itgsubstlem  23811  dgrlem  23985  ulmshftlem  24143  ulm0  24145  ulmcau  24149  iblulm  24161  rlimcnp  24692  xrlimcnp  24695  fsumdvdsmul  24921  chtub  24937  2sqlem10  25153  dchrisum0flb  25199  pntpbnd1  25275  pntpbnd  25277  pntibndlem2  25280  pntibndlem3  25281  pntibnd  25282  pntlemi  25293  pntleme  25297  pntlem3  25298  pntlemp  25299  pntleml  25300  pnt3  25301  istrkgld  25358  trgcgrg  25410  tgcgr4  25426  isperp  25607  brbtwn  25779  usgruspgrb  26076  usgr1e  26137  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  nbgr0vtx  26252  nbgr1vtx  26254  uvtxa01vtx0  26297  cplgr1v  26326  cusgrexi  26339  1hevtxdg0  26401  wlkeq  26529  wlkl1loop  26534  uspgr2wlkeq  26542  upgr2wlk  26564  redwlk  26569  wlkp1lem8  26577  usgr2wlkneq  26652  usgr2trlncl  26656  usgr2pthlem  26659  usgr2pth  26660  pthdlem1  26662  uspgrn2crct  26700  crctcshwlkn0lem7  26708  crctcshwlkn0  26713  wwlknp  26734  wwlksn0s  26746  wlkiswwlks1  26753  wlkiswwlks2lem4  26758  wlkiswwlksupgr2  26763  wlknewwlksn  26773  wwlksnred  26787  wwlksnext  26788  rusgrnumwwlkl1  26863  clwwlknp  26887  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a  26899  clwlkclwwlklem3  26902  clwwlkinwwlk  26905  clwwlksn2  26910  clwwlksel  26914  clwwlksf  26915  wwlksext2clwwlk  26924  wwlksubclwwlks  26925  clwlksfclwwlk  26962  clwlksf1clwwlklem  26968  1ewlk  26976  1wlkdlem4  27000  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  dfconngr1  27048  isconngr1  27050  frgr3v  27139  frgrwopregasn  27180  frgrwopregbsn  27181  numclwwlkovf2ex  27219  ubth  27729  acunirnmpt2  29460  acunirnmpt2f  29461  aciunf1  29463  lmxrge0  29998  sigaclcu3  30185  measval  30261  isrnmeas  30263  sitgval  30394  eulerpartlemsv3  30423  eulerpartlemo  30427  eulerpartlemn  30443  bnj1514  31131  subfacp1lem3  31164  subfacp1lem5  31166  txpconn  31214  cvxpconn  31224  cvmscbv  31240  cvmsi  31247  cvmsval  31248  elmrsubrn  31417  frinsg  31742  bj-raldifsn  33054  poimirlem1  33410  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  poimirlem32  33441  heicant  33444  mblfinlem3  33448  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  cnicciblnc  33481  sdclem1  33539  fdc  33541  rrncmslem  33631  isass  33645  exidreslem  33676  exidresid  33678  isrngod  33697  isgrpda  33754  iscom2  33794  pautsetN  35384  tendofset  36046  tendoset  36047  hdmap14lem13  37172  kelac1  37633  gicabl  37669  lpirlnr  37687  fiinfi  37878  clsk1independent  38344  wessf1ornlem  39371  uzub  39658  mccl  39830  climsuse  39840  limsupmnfuzlem  39958  limsupmnfuz  39959  limsupre3uzlem  39967  limsupre3uz  39968  limsupreuz  39969  0cnv  39974  climuz  39976  lmbr3  39979  limsupgt  40010  liminflt  40037  xlimmnf  40067  xlimpnf  40068  xlimmnfmpt  40069  xlimpnfmpt  40070  dfxlim2  40074  fourierdlem2  40326  fourierdlem3  40327  fourierdlem31  40355  fourierdlem47  40370  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem80  40403  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  etransclem48  40499  etransc  40500  ismea  40668  caragenval  40707  omessle  40712  smfmullem2  40999  smfmul  41002  2ffzoeq  41338  iccpval  41351  iccpartigtl  41359  pfxeq  41404  pfxsuffeqwrdeq  41406  pfx2  41412  c0snmgmhm  41914  linds0  42254  lindsrng01  42257