Theorem raleqdv 3292

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ral 3048  df-rex 3057

This theorem is referenced by:  raleqtrdv  3294  raleqtrrdv  3296  raleqbidva  3298  raleleqOLD  3309  raldifeq  4441  frpoinsg  6290  f12dfv  7207  f13dfv  7208  cbvfo  7223  isoselem  7275  ofrfvalg  7618  omsinds  7817  frpoins3xpg  8070  frpoins3xp3g  8071  frrlem4  8219  issmo2  8269  smoeq  8270  on2ind  8584  on3ind  8585  naddsuc2  8616  frfi  9169  marypha1lem  9317  marypha1  9318  dfoi  9397  oieq2  9399  ordtypecbv  9403  ordtypelem2  9405  ordtypelem3  9406  ordtypelem9  9412  wemapwe  9587  ttrclss  9610  ttrclselem2  9616  frinsg  9644  tcrank  9777  isacn  9935  pwsdompw  10094  isfin2  10185  isfin3ds  10220  isf33lem  10257  hsmexlem4  10320  zorn2lem6  10392  zorn2lem7  10393  zorn2g  10394  fpwwe2lem12  10533  uzsupss  12838  fzrevral2  13513  fzrevral3  13514  fzshftral  13515  fzoshftral  13687  uzsinds  13894  expmulnbnd  14142  eqs1  14520  swrdspsleq  14573  pfxeq  14603  pfxsuffeqwrdeq  14605  repswsymballbi  14687  cshw1  14729  pfx2  14854  wwlktovf1  14864  eqwrds3  14868  rexuz3  15256  rexuzre  15260  limsupgle  15384  rlim  15402  climconst  15450  rlimclim1  15452  climshftlem  15481  isercoll  15575  caucvgb  15587  serf0  15588  mertenslem1  15791  coprmprod  16572  coprmproddvds  16574  prmind2  16596  vdwlem10  16902  vdwlem13  16905  vdwnnlem2  16908  vdwnnlem3  16909  vdwnn  16910  ramval  16920  ramz  16937  prmgaplem5  16967  isacs  17557  cidpropd  17616  monpropd  17644  isssc  17727  fullsubc  17757  funcpropd  17809  isfth  17823  fthpropd  17830  grpidpropd  18570  sgrppropd  18639  mndpropd  18667  nmznsg  19080  ghmnsgima  19152  symgextfo  19334  gsmsymgrfixlem1  19339  gsmsymgrfix  19340  fvcosymgeq  19341  gsmsymgreqlem2  19343  psgnunilem3  19408  sylow2blem3  19534  sylow3lem6  19544  cmnpropd  19703  telgsumfzs  19901  rngpropd  20092  ringpropd  20206  c0snmgmhm  20380  abvpropd  20750  lsspropd  20951  lmhmpropd  21007  lbspropd  21033  pj1lmhm  21034  psgndiflemB  21537  phlpropd  21592  islindf  21749  lindfmm  21764  islindf4  21775  islindf5  21776  assapropd  21809  scmatf1  22446  isclo  23002  lmfval  23147  lmconst  23176  iscnrm2  23253  ist0-2  23259  ist1-2  23262  ishaus2  23266  subislly  23396  elpt  23487  elptr  23488  ptbasfi  23496  fclscmp  23945  ufilcmp  23947  cnpfcf  23956  alexsubALTlem1  23962  alexsubALTlem2  23963  alexsubALTlem4  23965  tmdgsum2  24011  tsmsf1o  24060  ustval  24118  ucnval  24191  imasdsf1olem  24288  imasf1oxmet  24290  imasf1omet  24291  metss  24423  prdsxmslem2  24444  lebnumlem3  24889  ishtpy  24898  lmnn  25190  evthicc  25387  cniccbdd  25389  ovolicc2lem4  25448  0pledm  25601  cniccibl  25769  cnicciblnc  25771  c1lip1  25929  lhop1  25946  itgsubstlem  25982  ulmshftlem  26325  ulm0  26327  ulmcau  26331  rlimcnp  26902  fsumdvdsmul  27132  fsumdvdsmulOLD  27134  chtub  27150  2sqlem10  27366  dchrisum0flb  27448  pntpbnd1  27524  pntpbnd  27526  pntibndlem2  27529  pntibndlem3  27530  pntibnd  27531  pntlemi  27542  pntleme  27546  pntlem3  27547  pntlemp  27548  pntleml  27549  pnt3  27550  madebdaylemlrcut  27844  noinds  27888  no2indslem  27897  no3inds  27901  precsexlem9  28153  istrkgld  28437  trgcgrg  28493  tgcgr4  28509  isperp  28690  brbtwn  28877  usgruspgrb  29161  nbgr2vtx1edg  29328  nbuhgr2vtx1edgb  29330  nbgr1vtx  29336  uvtx01vtx  29375  cplgr1v  29408  wlkeq  29612  wlkl1loop  29616  uspgr2wlkeq  29624  upgr2wlk  29645  redwlk  29649  wlkp1lem8  29657  usgr2wlkneq  29734  usgr2trlncl  29738  usgr2pthlem  29741  usgr2pth  29742  pthdlem1  29744  uspgrn2crct  29786  crctcshwlkn0  29799  wwlknp  29821  wwlksn0s  29839  wlkiswwlks1  29845  wlkiswwlks2lem4  29850  wwlksnred  29870  rusgrnumwwlkl1  29949  clwwlkccatlem  29969  clwlkclwwlklem2a1  29972  clwlkclwwlklem2a  29978  clwlkclwwlklem3  29981  clwwlkn  30006  clwwlknp  30017  clwwlkinwwlk  30020  clwwlkn1  30021  clwwlkn2  30024  clwwlkel  30026  clwwlkf  30027  clwwlkwwlksb  30034  1ewlk  30095  upgr3v3e3cycl  30160  upgr4cycl4dv4e  30165  dfconngr1  30168  isconngr1  30170  frgr3v  30255  frgrwopregasn  30296  frgrwopregbsn  30297  ubth  30853  acunirnmpt2  32642  acunirnmpt2f  32643  aciunf1  32645  fnpreimac  32653  fxpgaval  33136  crngmxidl  33434  lmxrge0  33965  measval  34211  isrnmeas  34213  sitgval  34345  eulerpartlemo  34378  eulerpartlemn  34394  onvf1odlem4  35150  subfacp1lem3  35226  subfacp1lem5  35228  txpconn  35276  cvxpconn  35286  cvmscbv  35302  cvmsi  35309  cvmsval  35310  satf  35397  sat1el2xp  35423  elmrsubrn  35564  weiunlem2  36507  bj-raldifsn  37144  poimirlem26  37685  poimirlem27  37686  poimirlem31  37690  poimirlem32  37691  heicant  37694  mblfinlem3  37698  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  sdclem1  37782  fdc  37784  rrncmslem  37871  isass  37885  isrngod  37937  isgrpda  37994  iscom2  38034  pautsetN  40196  tendofset  40856  tendoset  40857  hdmap14lem13  41978  3factsumint1  42113  sticksstones3  42240  kelac1  43155  gicabl  43191  cantnfresb  43416  safesnsupfilb  43510  fiinfi  43665  clsk1independent  44138  scotteqd  44329  wessf1ornlem  45281  uzub  45528  rexanuz2nf  45589  mccl  45697  climsuse  45707  limsupmnfuzlem  45823  limsupmnfuz  45824  limsupre3uzlem  45832  limsupre3uz  45833  limsupreuz  45834  0cnv  45839  climuz  45841  lmbr3  45844  limsupgt  45875  liminflt  45902  xlimpnfxnegmnf  45911  xlimmnf  45938  xlimpnf  45939  xlimmnfmpt  45940  xlimpnfmpt  45941  dfxlim2  45945  fourierdlem2  46206  fourierdlem3  46207  fourierdlem31  46235  fourierdlem47  46250  fourierdlem70  46273  fourierdlem71  46274  fourierdlem80  46283  fourierdlem103  46306  fourierdlem104  46307  fourierdlem113  46316  etransclem48  46379  etransc  46380  caragenval  46590  omessle  46595  smfmullem2  46889  smfmul  46892  2ffzoeq  47426  iccpval  47514  iccpartigtl  47522  cycl3grtrilem  48045  grlimedgclnbgr  48094  grlimgrtri  48102  grilcbri2  48110  usgrexmpl2trifr  48136  gpg5nbgrvtx03star  48179  gpg5nbgr3star  48180  lindsrng01  48568  rrx2line  48840  initopropd  49343  termopropd  49344  fucofulem2  49411  thincpropd  49542  isinito2lem  49598