Theorem raleqdv 3289

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  raleqtrdv  3291  raleqtrrdv  3293  raleqbidva  3295  raleleqOLD  3306  raldifeq  4445  frpoinsg  6291  f12dfv  7210  f13dfv  7211  cbvfo  7226  isoselem  7278  ofrfvalg  7621  omsinds  7820  frpoins3xpg  8073  frpoins3xp3g  8074  frrlem4  8222  issmo2  8272  smoeq  8273  on2ind  8587  on3ind  8588  naddsuc2  8619  frfi  9174  marypha1lem  9323  marypha1  9324  dfoi  9403  oieq2  9405  ordtypecbv  9409  ordtypelem2  9411  ordtypelem3  9412  ordtypelem9  9418  wemapwe  9593  ttrclss  9616  ttrclselem2  9622  frinsg  9647  tcrank  9780  isacn  9938  pwsdompw  10097  isfin2  10188  isfin3ds  10223  isf33lem  10260  hsmexlem4  10323  zorn2lem6  10395  zorn2lem7  10396  zorn2g  10397  fpwwe2lem12  10536  uzsupss  12841  fzrevral2  13516  fzrevral3  13517  fzshftral  13518  fzoshftral  13687  uzsinds  13894  expmulnbnd  14142  eqs1  14519  swrdspsleq  14572  pfxeq  14602  pfxsuffeqwrdeq  14604  repswsymballbi  14686  cshw1  14728  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  18536  sgrppropd  18605  mndpropd  18633  nmznsg  19047  ghmnsgima  19119  symgextfo  19301  gsmsymgrfixlem1  19306  gsmsymgrfix  19307  fvcosymgeq  19308  gsmsymgreqlem2  19310  psgnunilem3  19375  sylow2blem3  19501  sylow3lem6  19511  cmnpropd  19670  telgsumfzs  19868  rngpropd  20059  ringpropd  20173  c0snmgmhm  20347  abvpropd  20720  lsspropd  20921  lmhmpropd  20977  lbspropd  21003  pj1lmhm  21004  psgndiflemB  21507  phlpropd  21562  islindf  21719  lindfmm  21734  islindf4  21745  islindf5  21746  assapropd  21779  scmatf1  22416  isclo  22972  lmfval  23117  lmconst  23146  iscnrm2  23223  ist0-2  23229  ist1-2  23232  ishaus2  23236  subislly  23366  elpt  23457  elptr  23458  ptbasfi  23466  fclscmp  23915  ufilcmp  23917  cnpfcf  23926  alexsubALTlem1  23932  alexsubALTlem2  23933  alexsubALTlem4  23935  tmdgsum2  23981  tsmsf1o  24030  ustval  24088  ucnval  24162  imasdsf1olem  24259  imasf1oxmet  24261  imasf1omet  24262  metss  24394  prdsxmslem2  24415  lebnumlem3  24860  ishtpy  24869  lmnn  25161  evthicc  25358  cniccbdd  25360  ovolicc2lem4  25419  0pledm  25572  cniccibl  25740  cnicciblnc  25742  c1lip1  25900  lhop1  25917  itgsubstlem  25953  ulmshftlem  26296  ulm0  26298  ulmcau  26302  rlimcnp  26873  fsumdvdsmul  27103  fsumdvdsmulOLD  27105  chtub  27121  2sqlem10  27337  dchrisum0flb  27419  pntpbnd1  27495  pntpbnd  27497  pntibndlem2  27500  pntibndlem3  27501  pntibnd  27502  pntlemi  27513  pntleme  27517  pntlem3  27518  pntlemp  27519  pntleml  27520  pnt3  27521  madebdaylemlrcut  27813  noinds  27857  no2indslem  27866  no3inds  27870  precsexlem9  28122  istrkgld  28404  trgcgrg  28460  tgcgr4  28476  isperp  28657  brbtwn  28844  usgruspgrb  29128  nbgr2vtx1edg  29295  nbuhgr2vtx1edgb  29297  nbgr1vtx  29303  uvtx01vtx  29342  cplgr1v  29375  wlkeq  29579  wlkl1loop  29583  uspgr2wlkeq  29591  upgr2wlk  29612  redwlk  29616  wlkp1lem8  29624  usgr2wlkneq  29701  usgr2trlncl  29705  usgr2pthlem  29708  usgr2pth  29709  pthdlem1  29711  uspgrn2crct  29753  crctcshwlkn0  29766  wwlknp  29788  wwlksn0s  29806  wlkiswwlks1  29812  wlkiswwlks2lem4  29817  wwlksnred  29837  rusgrnumwwlkl1  29913  clwwlkccatlem  29933  clwlkclwwlklem2a1  29936  clwlkclwwlklem2a  29942  clwlkclwwlklem3  29945  clwwlkn  29970  clwwlknp  29981  clwwlkinwwlk  29984  clwwlkn1  29985  clwwlkn2  29988  clwwlkel  29990  clwwlkf  29991  clwwlkwwlksb  29998  1ewlk  30059  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  dfconngr1  30132  isconngr1  30134  frgr3v  30219  frgrwopregasn  30260  frgrwopregbsn  30261  ubth  30817  acunirnmpt2  32604  acunirnmpt2f  32605  aciunf1  32607  fnpreimac  32615  fxpgaval  33110  crngmxidl  33407  lmxrge0  33925  measval  34171  isrnmeas  34173  sitgval  34306  eulerpartlemo  34339  eulerpartlemn  34355  onvf1odlem4  35089  subfacp1lem3  35165  subfacp1lem5  35167  txpconn  35215  cvxpconn  35225  cvmscbv  35241  cvmsi  35248  cvmsval  35249  satf  35336  sat1el2xp  35362  elmrsubrn  35503  weiunlem2  36447  bj-raldifsn  37084  poimirlem26  37636  poimirlem27  37637  poimirlem31  37641  poimirlem32  37642  heicant  37645  mblfinlem3  37649  ovoliunnfl  37652  voliunnfl  37654  volsupnfl  37655  sdclem1  37733  fdc  37735  rrncmslem  37822  isass  37836  isrngod  37888  isgrpda  37945  iscom2  37985  pautsetN  40087  tendofset  40747  tendoset  40748  hdmap14lem13  41869  3factsumint1  42004  sticksstones3  42131  kelac1  43046  gicabl  43082  cantnfresb  43307  safesnsupfilb  43401  fiinfi  43556  clsk1independent  44029  scotteqd  44220  wessf1ornlem  45173  uzub  45420  rexanuz2nf  45481  mccl  45589  climsuse  45599  limsupmnfuzlem  45717  limsupmnfuz  45718  limsupre3uzlem  45726  limsupre3uz  45727  limsupreuz  45728  0cnv  45733  climuz  45735  lmbr3  45738  limsupgt  45769  liminflt  45796  xlimpnfxnegmnf  45805  xlimmnf  45832  xlimpnf  45833  xlimmnfmpt  45834  xlimpnfmpt  45835  dfxlim2  45839  fourierdlem2  46100  fourierdlem3  46101  fourierdlem31  46129  fourierdlem47  46144  fourierdlem70  46167  fourierdlem71  46168  fourierdlem80  46177  fourierdlem103  46200  fourierdlem104  46201  fourierdlem113  46210  etransclem48  46273  etransc  46274  caragenval  46484  omessle  46489  smfmullem2  46783  smfmul  46786  2ffzoeq  47321  iccpval  47409  iccpartigtl  47417  cycl3grtrilem  47940  grlimedgclnbgr  47989  grlimgrtri  47997  grilcbri2  48005  usgrexmpl2trifr  48031  gpg5nbgrvtx03star  48074  gpg5nbgr3star  48075  lindsrng01  48463  rrx2line  48735  initopropd  49238  termopropd  49239  fucofulem2  49306  thincpropd  49437  isinito2lem  49493