Theorem raleqdv 3297

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

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

Proof of Theorem raleqdv

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ral 3053  df-rex 3062

This theorem is referenced by:  raleqtrdv  3299  raleqtrrdv  3301  raleqbidva  3303  raleleqOLD  3314  raldifeq  4447  frpoinsg  6302  f12dfv  7221  f13dfv  7222  cbvfo  7237  isoselem  7289  ofrfvalg  7632  omsinds  7831  frpoins3xpg  8084  frpoins3xp3g  8085  frrlem4  8233  issmo2  8283  smoeq  8284  on2ind  8599  on3ind  8600  naddsuc2  8631  frfi  9189  marypha1lem  9340  marypha1  9341  dfoi  9420  oieq2  9422  ordtypecbv  9426  ordtypelem2  9428  ordtypelem3  9429  ordtypelem9  9435  wemapwe  9610  ttrclss  9633  ttrclselem2  9639  frinsg  9667  tcrank  9800  isacn  9958  pwsdompw  10117  isfin2  10208  isfin3ds  10243  isf33lem  10280  hsmexlem4  10343  zorn2lem6  10415  zorn2lem7  10416  zorn2g  10417  fpwwe2lem12  10557  uzsupss  12857  fzrevral2  13533  fzrevral3  13534  fzshftral  13535  fzoshftral  13707  uzsinds  13914  expmulnbnd  14162  eqs1  14540  swrdspsleq  14593  pfxeq  14623  pfxsuffeqwrdeq  14625  repswsymballbi  14707  cshw1  14749  pfx2  14874  wwlktovf1  14884  eqwrds3  14888  rexuz3  15276  rexuzre  15280  limsupgle  15404  rlim  15422  climconst  15470  rlimclim1  15472  climshftlem  15501  isercoll  15595  caucvgb  15607  serf0  15608  mertenslem1  15811  coprmprod  16592  coprmproddvds  16594  prmind2  16616  vdwlem10  16922  vdwlem13  16925  vdwnnlem2  16928  vdwnnlem3  16929  vdwnn  16930  ramval  16940  ramz  16957  prmgaplem5  16987  isacs  17578  cidpropd  17637  monpropd  17665  isssc  17748  fullsubc  17778  funcpropd  17830  isfth  17844  fthpropd  17851  grpidpropd  18591  sgrppropd  18660  mndpropd  18688  nmznsg  19101  ghmnsgima  19173  symgextfo  19355  gsmsymgrfixlem1  19360  gsmsymgrfix  19361  fvcosymgeq  19362  gsmsymgreqlem2  19364  psgnunilem3  19429  sylow2blem3  19555  sylow3lem6  19565  cmnpropd  19724  telgsumfzs  19922  rngpropd  20113  ringpropd  20227  c0snmgmhm  20402  abvpropd  20772  lsspropd  20973  lmhmpropd  21029  lbspropd  21055  pj1lmhm  21056  psgndiflemB  21559  phlpropd  21614  islindf  21771  lindfmm  21786  islindf4  21797  islindf5  21798  assapropd  21831  scmatf1  22479  isclo  23035  lmfval  23180  lmconst  23209  iscnrm2  23286  ist0-2  23292  ist1-2  23295  ishaus2  23299  subislly  23429  elpt  23520  elptr  23521  ptbasfi  23529  fclscmp  23978  ufilcmp  23980  cnpfcf  23989  alexsubALTlem1  23995  alexsubALTlem2  23996  alexsubALTlem4  23998  tmdgsum2  24044  tsmsf1o  24093  ustval  24151  ucnval  24224  imasdsf1olem  24321  imasf1oxmet  24323  imasf1omet  24324  metss  24456  prdsxmslem2  24477  lebnumlem3  24922  ishtpy  24931  lmnn  25223  evthicc  25420  cniccbdd  25422  ovolicc2lem4  25481  0pledm  25634  cniccibl  25802  cnicciblnc  25804  c1lip1  25962  lhop1  25979  itgsubstlem  26015  ulmshftlem  26358  ulm0  26360  ulmcau  26364  rlimcnp  26935  fsumdvdsmul  27165  fsumdvdsmulOLD  27167  chtub  27183  2sqlem10  27399  dchrisum0flb  27481  pntpbnd1  27557  pntpbnd  27559  pntibndlem2  27562  pntibndlem3  27563  pntibnd  27564  pntlemi  27575  pntleme  27579  pntlem3  27580  pntlemp  27581  pntleml  27582  pnt3  27583  madebdaylemlrcut  27899  noinds  27945  no2indlesm  27954  no3inds  27958  precsexlem9  28215  istrkgld  28535  trgcgrg  28591  tgcgr4  28607  isperp  28788  brbtwn  28976  usgruspgrb  29260  nbgr2vtx1edg  29427  nbuhgr2vtx1edgb  29429  nbgr1vtx  29435  uvtx01vtx  29474  cplgr1v  29507  wlkeq  29711  wlkl1loop  29715  uspgr2wlkeq  29723  upgr2wlk  29744  redwlk  29748  wlkp1lem8  29756  usgr2wlkneq  29833  usgr2trlncl  29837  usgr2pthlem  29840  usgr2pth  29841  pthdlem1  29843  uspgrn2crct  29885  crctcshwlkn0  29898  wwlknp  29920  wwlksn0s  29938  wlkiswwlks1  29944  wlkiswwlks2lem4  29949  wwlksnred  29969  rusgrnumwwlkl1  30048  clwwlkccatlem  30068  clwlkclwwlklem2a1  30071  clwlkclwwlklem2a  30077  clwlkclwwlklem3  30080  clwwlkn  30105  clwwlknp  30116  clwwlkinwwlk  30119  clwwlkn1  30120  clwwlkn2  30123  clwwlkel  30125  clwwlkf  30126  clwwlkwwlksb  30133  1ewlk  30194  upgr3v3e3cycl  30259  upgr4cycl4dv4e  30264  dfconngr1  30267  isconngr1  30269  frgr3v  30354  frgrwopregasn  30395  frgrwopregbsn  30396  ubth  30952  acunirnmpt2  32741  acunirnmpt2f  32742  aciunf1  32744  fnpreimac  32751  fxpgaval  33251  crngmxidl  33552  lmxrge0  34111  measval  34357  isrnmeas  34359  sitgval  34491  eulerpartlemo  34524  eulerpartlemn  34540  onvf1odlem4  35302  subfacp1lem3  35378  subfacp1lem5  35380  txpconn  35428  cvxpconn  35438  cvmscbv  35454  cvmsi  35461  cvmsval  35462  satf  35549  sat1el2xp  35575  elmrsubrn  35716  weiunlem  36659  bj-raldifsn  37307  poimirlem26  37849  poimirlem27  37850  poimirlem31  37854  poimirlem32  37855  heicant  37858  mblfinlem3  37862  ovoliunnfl  37865  voliunnfl  37867  volsupnfl  37868  sdclem1  37946  fdc  37948  rrncmslem  38035  isass  38049  isrngod  38101  isgrpda  38158  iscom2  38198  pautsetN  40426  tendofset  41086  tendoset  41087  hdmap14lem13  42208  3factsumint1  42343  sticksstones3  42470  kelac1  43372  gicabl  43408  cantnfresb  43633  safesnsupfilb  43726  fiinfi  43881  clsk1independent  44354  scotteqd  44545  wessf1ornlem  45496  uzub  45742  rexanuz2nf  45803  mccl  45911  climsuse  45921  limsupmnfuzlem  46037  limsupmnfuz  46038  limsupre3uzlem  46046  limsupre3uz  46047  limsupreuz  46048  0cnv  46053  climuz  46055  lmbr3  46058  limsupgt  46089  liminflt  46116  xlimpnfxnegmnf  46125  xlimmnf  46152  xlimpnf  46153  xlimmnfmpt  46154  xlimpnfmpt  46155  dfxlim2  46159  fourierdlem2  46420  fourierdlem3  46421  fourierdlem31  46449  fourierdlem47  46464  fourierdlem70  46487  fourierdlem71  46488  fourierdlem80  46497  fourierdlem103  46520  fourierdlem104  46521  fourierdlem113  46530  etransclem48  46593  etransc  46594  caragenval  46804  omessle  46809  smfmullem2  47103  smfmul  47106  2ffzoeq  47640  iccpval  47728  iccpartigtl  47736  cycl3grtrilem  48259  grlimedgclnbgr  48308  grlimgrtri  48316  grilcbri2  48324  usgrexmpl2trifr  48350  gpg5nbgrvtx03star  48393  gpg5nbgr3star  48394  lindsrng01  48781  rrx2line  49053  initopropd  49555  termopropd  49556  fucofulem2  49623  thincpropd  49754  isinito2lem  49810