Theorem raleqdv 3349

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

Hypothesis

Ref	Expression
raleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
raleqdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		raleq 3343	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ral 3070

This theorem is referenced by:  raleqbidva  3355  raleleqALT  3358  raldifeq  4425  frpoinsg  6250  wfisgOLD  6261  fveqressseq  6966  f12dfv  7154  f13dfv  7155  cbvfo  7170  isoselem  7221  ofrfvalg  7550  omsinds  7742  omsindsOLD  7743  frrlem4  8114  wfrlem4OLD  8152  issmo2  8189  smoeq  8190  frfi  9068  marypha1lem  9201  marypha1  9202  dfoi  9279  oieq2  9281  ordtypecbv  9285  ordtypelem2  9287  ordtypelem3  9288  ordtypelem9  9294  wemapwe  9464  ttrclss  9487  ttrclselem2  9493  frinsg  9518  tcrank  9651  isacn  9809  pwsdompw  9969  isfin2  10059  isfin3ds  10094  isf33lem  10131  hsmexlem4  10194  zorn2lem6  10266  zorn2lem7  10267  zorn2g  10268  fpwwe2lem12  10407  uzsupss  12689  fzrevral2  13351  fzrevral3  13352  fzshftral  13353  fzoshftral  13513  uzsinds  13716  expmulnbnd  13959  eqs1  14326  swrdspsleq  14387  pfxeq  14418  pfxsuffeqwrdeq  14420  repswsymballbi  14502  cshw1  14544  pfx2  14669  wwlktovf1  14681  eqwrds3  14685  rexuz3  15069  rexuzre  15073  limsupgle  15195  rlim  15213  climconst  15261  rlimclim1  15263  climshftlem  15292  isercoll  15388  caucvgb  15400  serf0  15401  mertenslem1  15605  coprmprod  16375  coprmproddvds  16377  prmind2  16399  vdwlem10  16700  vdwlem13  16703  vdwnnlem2  16706  vdwnnlem3  16707  vdwnn  16708  ramval  16718  ramz  16735  prmgaplem5  16765  isacs  17369  cidpropd  17428  monpropd  17458  isssc  17541  fullsubc  17574  funcpropd  17625  isfth  17639  fthpropd  17646  grpidpropd  18355  mndpropd  18419  nmznsg  18805  ghmnsgima  18867  symgextfo  19039  gsmsymgrfixlem1  19044  gsmsymgrfix  19045  fvcosymgeq  19046  gsmsymgreqlem2  19048  symgfixf1  19054  psgnunilem3  19113  subgpgp  19211  sylow2blem3  19236  sylow3lem6  19246  efgsp1  19352  efgsres  19353  cmnpropd  19405  telgsumfzs  19599  ablfac2  19701  ringpropd  19830  abvpropd  20111  lsspropd  20288  lmhmpropd  20344  lbspropd  20370  pj1lmhm  20371  znf1o  20768  psgndiflemB  20814  phlpropd  20869  islindf  21028  lindfmm  21043  islindf4  21054  islindf5  21055  assapropd  21085  scmatf1  21689  isclo  22247  perfopn  22345  lmfval  22392  lmconst  22421  cncnp  22440  iscnrm2  22498  ist0-2  22504  ist1-2  22507  ishaus2  22511  ordtt1  22539  subislly  22641  elpt  22732  elptr  22733  ptbasfi  22741  tx1stc  22810  xkococnlem  22819  fclscmp  23190  ufilcmp  23192  cnpfcf  23201  alexsubALTlem1  23207  alexsubALTlem2  23208  alexsubALTlem4  23210  tmdgsum2  23256  tsmsf1o  23305  ustval  23363  ucnval  23438  imasdsf1olem  23535  imasf1oxmet  23537  imasf1omet  23538  metss  23673  prdsxmslem2  23694  cnmpopc  24100  lebnumlem3  24135  ishtpy  24144  pi1coghm  24233  lmnn  24436  evthicc  24632  cniccbdd  24634  ovolicc2lem4  24693  0pledm  24846  cniccibl  25014  cnicciblnc  25016  c1lip1  25170  dvivthlem1  25181  lhop1  25187  itgsubstlem  25221  dgrlem  25399  ulmshftlem  25557  ulm0  25559  ulmcau  25563  iblulm  25575  rlimcnp  26124  xrlimcnp  26127  fsumdvdsmul  26353  chtub  26369  2sqlem10  26585  dchrisum0flb  26667  pntpbnd1  26743  pntpbnd  26745  pntibndlem2  26748  pntibndlem3  26749  pntibnd  26750  pntlemi  26761  pntleme  26765  pntlem3  26766  pntlemp  26767  pntleml  26768  pnt3  26769  istrkgld  26829  trgcgrg  26885  tgcgr4  26901  isperp  27082  brbtwn  27276  usgruspgrb  27560  usgr1e  27621  nbgr2vtx1edg  27726  nbuhgr2vtx1edgb  27728  nbgr0vtx  27732  nbgr1vtx  27734  uvtx01vtx  27773  cplgr1v  27806  cusgrexi  27819  1hevtxdg0  27881  wlkeq  28010  wlkl1loop  28014  uspgr2wlkeq  28022  upgr2wlk  28045  redwlk  28049  wlkp1lem8  28057  usgr2wlkneq  28133  usgr2trlncl  28137  usgr2pthlem  28140  usgr2pth  28141  pthdlem1  28143  uspgrn2crct  28182  crctcshwlkn0lem7  28190  crctcshwlkn0  28195  wwlknp  28217  wwlksn0s  28235  wlkiswwlks1  28241  wlkiswwlks2lem4  28246  wlkiswwlksupgr2  28251  wlknewwlksn  28261  wwlksnred  28266  wwlksnext  28267  rusgrnumwwlkl1  28342  clwwlkccatlem  28362  clwlkclwwlklem2a1  28365  clwlkclwwlklem2a  28371  clwlkclwwlklem3  28374  clwlkclwwlkf1lem3  28379  clwwlkn  28399  clwwlknp  28410  clwwlkinwwlk  28413  clwwlkn1  28414  clwwlkn2  28417  clwwlkel  28419  clwwlkf  28420  clwwlkwwlksb  28427  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  clwwlknonex2  28482  1ewlk  28488  1wlkdlem4  28513  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  dfconngr1  28561  isconngr1  28563  frgr3v  28648  frgrwopregasn  28689  frgrwopregbsn  28690  ubth  29244  acunirnmpt2  31006  acunirnmpt2f  31007  aciunf1  31009  fnpreimac  31017  lmxrge0  31911  sigaclcu3  32099  measval  32175  isrnmeas  32177  sitgval  32308  eulerpartlemsv3  32337  eulerpartlemo  32341  eulerpartlemn  32357  bnj1514  33052  subfacp1lem3  33153  subfacp1lem5  33155  txpconn  33203  cvxpconn  33213  cvmscbv  33229  cvmsi  33236  cvmsval  33237  satf  33324  sat1el2xp  33350  elmrsubrn  33491  frpoins3xpg  33796  frpoins3xp3g  33797  on2ind  33837  on3ind  33838  madebdaylemlrcut  34088  noinds  34111  no2indslem  34120  no3inds  34124  bj-raldifsn  35280  poimirlem1  35787  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  poimirlem32  35818  heicant  35821  mblfinlem3  35825  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  sdclem1  35910  fdc  35912  rrncmslem  35999  isass  36013  exidreslem  36044  exidresid  36046  isrngod  36065  isgrpda  36122  iscom2  36162  pautsetN  38119  tendofset  38779  tendoset  38780  hdmap14lem13  39901  3factsumint1  40036  sticksstones3  40111  kelac1  40895  gicabl  40931  lpirlnr  40949  fiinfi  41187  clsk1independent  41663  scotteqd  41862  wessf1ornlem  42729  uzub  42978  mccl  43146  climsuse  43156  limsupmnfuzlem  43274  limsupmnfuz  43275  limsupre3uzlem  43283  limsupre3uz  43284  limsupreuz  43285  0cnv  43290  climuz  43292  lmbr3  43295  limsupgt  43326  liminflt  43353  xlimpnfxnegmnf  43362  xlimmnf  43389  xlimpnf  43390  xlimmnfmpt  43391  xlimpnfmpt  43392  dfxlim2  43396  fourierdlem2  43657  fourierdlem3  43658  fourierdlem31  43686  fourierdlem47  43701  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem80  43734  fourierdlem103  43757  fourierdlem104  43758  fourierdlem113  43767  etransclem48  43830  etransc  43831  caragenval  44038  omessle  44043  smfmullem2  44337  smfmul  44340  2ffzoeq  44831  iccpval  44878  iccpartigtl  44886  c0snmgmhm  45483  linds0  45817  lindsrng01  45820  rrx2line  46097