Theorem raleqdv 3315

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 3309	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-ral 3058

This theorem is referenced by:  raleqbidva  3321  raleleqALT  3324  raldifeq  4377  wfisg  6158  fveqressseq  6851  f12dfv  7035  f13dfv  7036  cbvfo  7050  isoselem  7101  ofrfvalg  7426  omsinds  7613  wfrlem4  7980  issmo2  8008  smoeq  8009  frfi  8830  marypha1lem  8963  marypha1  8964  dfoi  9041  oieq2  9043  ordtypecbv  9047  ordtypelem2  9049  ordtypelem3  9050  ordtypelem9  9056  wemapwe  9226  tcrank  9379  isacn  9537  pwsdompw  9697  isfin2  9787  isfin3ds  9822  isf33lem  9859  hsmexlem4  9922  zorn2lem6  9994  zorn2lem7  9995  zorn2g  9996  fpwwe2lem12  10135  uzsupss  12415  fzrevral2  13077  fzrevral3  13078  fzshftral  13079  fzoshftral  13238  uzsinds  13439  expmulnbnd  13681  eqs1  14048  swrdspsleq  14109  pfxeq  14140  pfxsuffeqwrdeq  14142  repswsymballbi  14224  cshw1  14266  pfx2  14391  wwlktovf1  14403  eqwrds3  14407  rexuz3  14791  rexuzre  14795  limsupgle  14917  rlim  14935  climconst  14983  rlimclim1  14985  climshftlem  15014  isercoll  15110  caucvgb  15122  serf0  15123  mertenslem1  15325  coprmprod  16095  coprmproddvds  16097  prmind2  16119  vdwlem10  16419  vdwlem13  16422  vdwnnlem2  16425  vdwnnlem3  16426  vdwnn  16427  ramval  16437  ramz  16454  prmgaplem5  16484  isacs  17018  cidpropd  17077  monpropd  17105  isssc  17188  fullsubc  17218  funcpropd  17268  isfth  17282  fthpropd  17289  grpidpropd  17981  mndpropd  18045  nmznsg  18431  ghmnsgima  18493  symgextfo  18661  gsmsymgrfixlem1  18666  gsmsymgrfix  18667  fvcosymgeq  18668  gsmsymgreqlem2  18670  symgfixf1  18676  psgnunilem3  18735  subgpgp  18833  sylow2blem3  18858  sylow3lem6  18868  efgsp1  18974  efgsres  18975  cmnpropd  19027  telgsumfzs  19221  ablfac2  19323  ringpropd  19447  abvpropd  19725  lsspropd  19901  lmhmpropd  19957  lbspropd  19983  pj1lmhm  19984  znf1o  20363  psgndiflemB  20409  phlpropd  20464  islindf  20621  lindfmm  20636  islindf4  20647  islindf5  20648  assapropd  20678  scmatf1  21275  isclo  21831  perfopn  21929  lmfval  21976  lmconst  22005  cncnp  22024  iscnrm2  22082  ist0-2  22088  ist1-2  22091  ishaus2  22095  ordtt1  22123  subislly  22225  elpt  22316  elptr  22317  ptbasfi  22325  tx1stc  22394  xkococnlem  22403  fclscmp  22774  ufilcmp  22776  cnpfcf  22785  alexsubALTlem1  22791  alexsubALTlem2  22792  alexsubALTlem4  22794  tmdgsum2  22840  tsmsf1o  22889  ustval  22947  ucnval  23022  imasdsf1olem  23119  imasf1oxmet  23121  imasf1omet  23122  metss  23254  prdsxmslem2  23275  cnmpopc  23673  lebnumlem3  23708  ishtpy  23717  pi1coghm  23806  lmnn  24008  evthicc  24204  cniccbdd  24206  ovolicc2lem4  24265  0pledm  24418  cniccibl  24585  cnicciblnc  24587  c1lip1  24741  dvivthlem1  24752  lhop1  24758  itgsubstlem  24792  dgrlem  24970  ulmshftlem  25128  ulm0  25130  ulmcau  25134  iblulm  25146  rlimcnp  25695  xrlimcnp  25698  fsumdvdsmul  25924  chtub  25940  2sqlem10  26156  dchrisum0flb  26238  pntpbnd1  26314  pntpbnd  26316  pntibndlem2  26319  pntibndlem3  26320  pntibnd  26321  pntlemi  26332  pntleme  26336  pntlem3  26337  pntlemp  26338  pntleml  26339  pnt3  26340  istrkgld  26397  trgcgrg  26453  tgcgr4  26469  isperp  26650  brbtwn  26837  usgruspgrb  27118  usgr1e  27179  nbgr2vtx1edg  27284  nbuhgr2vtx1edgb  27286  nbgr0vtx  27290  nbgr1vtx  27292  uvtx01vtx  27331  cplgr1v  27364  cusgrexi  27377  1hevtxdg0  27439  wlkeq  27567  wlkl1loop  27571  uspgr2wlkeq  27579  upgr2wlk  27602  redwlk  27606  wlkp1lem8  27614  usgr2wlkneq  27689  usgr2trlncl  27693  usgr2pthlem  27696  usgr2pth  27697  pthdlem1  27699  uspgrn2crct  27738  crctcshwlkn0lem7  27746  crctcshwlkn0  27751  wwlknp  27773  wwlksn0s  27791  wlkiswwlks1  27797  wlkiswwlks2lem4  27802  wlkiswwlksupgr2  27807  wlknewwlksn  27817  wwlksnred  27822  wwlksnext  27823  rusgrnumwwlkl1  27898  clwwlkccatlem  27918  clwlkclwwlklem2a1  27921  clwlkclwwlklem2a  27927  clwlkclwwlklem3  27930  clwlkclwwlkf1lem3  27935  clwwlkn  27955  clwwlknp  27966  clwwlkinwwlk  27969  clwwlkn1  27970  clwwlkn2  27973  clwwlkel  27975  clwwlkf  27976  clwwlkwwlksb  27983  wwlksext2clwwlk  27986  wwlksubclwwlk  27987  clwwlknonex2  28038  1ewlk  28044  1wlkdlem4  28069  upgr3v3e3cycl  28109  upgr4cycl4dv4e  28114  dfconngr1  28117  isconngr1  28119  frgr3v  28204  frgrwopregasn  28245  frgrwopregbsn  28246  ubth  28800  acunirnmpt2  30564  acunirnmpt2f  30565  aciunf1  30567  fnpreimac  30575  lmxrge0  31466  sigaclcu3  31652  measval  31728  isrnmeas  31730  sitgval  31861  eulerpartlemsv3  31890  eulerpartlemo  31894  eulerpartlemn  31910  bnj1514  32606  subfacp1lem3  32707  subfacp1lem5  32709  txpconn  32757  cvxpconn  32767  cvmscbv  32783  cvmsi  32790  cvmsval  32791  satf  32878  sat1el2xp  32904  elmrsubrn  33045  frpoinsg  33376  frpoins3xpg  33380  frpoins3xp3g  33381  frinsg  33385  frrlem4  33436  on2ind  33461  on3ind  33462  madebdaylemlrcut  33709  noinds  33731  no2indslem  33740  no3indslem  33744  bj-raldifsn  34881  poimirlem1  35390  poimirlem26  35415  poimirlem27  35416  poimirlem31  35420  poimirlem32  35421  heicant  35424  mblfinlem3  35428  ovoliunnfl  35431  voliunnfl  35433  volsupnfl  35434  sdclem1  35513  fdc  35515  rrncmslem  35602  isass  35616  exidreslem  35647  exidresid  35649  isrngod  35668  isgrpda  35725  iscom2  35765  pautsetN  37724  tendofset  38384  tendoset  38385  hdmap14lem13  39506  3factsumint1  39638  sticksstones3  39699  kelac1  40444  gicabl  40480  lpirlnr  40498  fiinfi  40709  clsk1independent  41186  scotteqd  41381  wessf1ornlem  42244  uzub  42493  mccl  42665  climsuse  42675  limsupmnfuzlem  42793  limsupmnfuz  42794  limsupre3uzlem  42802  limsupre3uz  42803  limsupreuz  42804  0cnv  42809  climuz  42811  lmbr3  42814  limsupgt  42845  liminflt  42872  xlimpnfxnegmnf  42881  xlimmnf  42908  xlimpnf  42909  xlimmnfmpt  42910  xlimpnfmpt  42911  dfxlim2  42915  fourierdlem2  43176  fourierdlem3  43177  fourierdlem31  43205  fourierdlem47  43220  fourierdlem70  43243  fourierdlem71  43244  fourierdlem73  43246  fourierdlem80  43253  fourierdlem103  43276  fourierdlem104  43277  fourierdlem113  43286  etransclem48  43349  etransc  43350  caragenval  43557  omessle  43562  smfmullem2  43849  smfmul  43852  2ffzoeq  44338  iccpval  44385  iccpartigtl  44393  c0snmgmhm  44990  linds0  45324  lindsrng01  45327  rrx2line  45604