Theorem raleqdv 3319

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ral 3077  df-rex 3087

This theorem is used by:  raleqtrdv  3321  raleqtrrdv  3323  raleqbidva  3325  raldifeq  4449  frpoinsg  6336  f12dfv  7270  f13dfv  7271  cbvfo  7286  isoselem  7338  ofrfvalg  7685  omsinds  7882  frpoins3xpg  8136  frpoins3xp3g  8137  frrlem4  8286  issmo2  8336  smoeq  8337  on2ind  8657  on3ind  8658  naddsuc2  8690  frfi  9255  marypha1lem  9403  marypha1  9404  dfoi  9483  oieq2  9485  ordtypecbv  9489  ordtypelem2  9491  ordtypelem3  9492  ordtypelem9  9498  wemapwe  9676  ttrclss  9699  ttrclselem2  9705  frinsg  9733  tcrank  9870  scotteqd  9887  isacn  10080  pwsdompw  10238  isfin2  10329  isfin3ds  10364  isf33lem  10401  hsmexlem4  10464  zorn2lem6  10536  zorn2lem7  10537  zorn2g  10538  fpwwe2lem12  10684  uzsupss  13022  fzrevral2  13701  fzrevral3  13702  fzshftral  13703  fzoshftral  13876  uzsinds  14084  expmulnbnd  14332  eqs1  14713  swrdspsleq  14768  pfxeq  14798  pfxsuffeqwrdeq  14800  repswsymballbi  14884  cshw1  14926  pfx2  15051  wwlktovf1  15063  eqwrds3  15067  rexuz3  15469  rexuzre  15473  limsupgle  15597  rlim  15615  climconst  15663  rlimclim1  15665  climshftlem  15694  isercoll  15788  caucvgb  15800  serf0  15801  mertenslem1  16006  coprmprod  16784  coprmproddvds  16786  prmind2  16808  vdwlem10  17115  vdwlem13  17118  vdwnnlem2  17121  vdwnnlem3  17122  vdwnn  17123  ramval  17133  ramz  17150  prmgaplem5  17180  isacs  17772  cidpropd  17831  monpropd  17859  isssc  17942  fullsubc  17972  funcpropd  18024  isfth  18038  fthpropd  18045  grpidpropd  18789  sgrppropd  18867  mndpropd  18898  nmznsg  19325  ghmnsgima  19401  symgextfo  19583  gsmsymgrfixlem1  19588  gsmsymgrfix  19589  fvcosymgeq  19590  gsmsymgreqlem2  19592  psgnunilem3  19657  sylow2blem3  19783  sylow3lem6  19793  cmnpropd  19952  telgsumfzs  20150  rngpropd  20343  ringpropd  20466  c0snmgmhm  20639  abvpropd  21039  lsspropd  21239  lmhmpropd  21295  lbspropd  21321  pj1lmhm  21322  psgndiflemB  21853  phlpropd  21908  islindf  22065  lindfmm  22080  islindf4  22091  islindf5  22092  assapropd  22126  scmatf1  22793  isclo  23352  lmfval  23497  lmconst  23526  iscnrm2  23603  ist0-2  23609  ist1-2  23612  ishaus2  23616  subislly  23747  elpt  23838  elptr  23839  ptbasfi  23847  fclscmp  24296  ufilcmp  24298  cnpfcf  24307  alexsubALTlem1  24313  alexsubALTlem2  24314  alexsubALTlem4  24316  tmdgsum2  24362  tsmsf1o  24411  ustval  24469  ucnval  24542  imasdsf1olem  24639  imasf1oxmet  24641  imasf1omet  24642  metss  24774  prdsxmslem2  24795  lebnumlem3  25231  ishtpy  25240  lmnn  25531  evthicc  25727  cniccbdd  25729  ovolicc2lem4  25788  0pledm  25941  cniccibl  26108  cnicciblnc  26110  c1lip1  26264  lhop1  26281  itgsubstlem  26315  ulmshftlem  26665  ulm0  26667  ulmcau  26671  rlimcnp  27242  fsumdvdsmul  27471  chtub  27488  2sqlem10  27704  dchrisum0flb  27786  pntpbnd1  27862  pntpbnd  27864  pntibndlem2  27867  pntibndlem3  27868  pntibnd  27869  pntlemi  27880  pntleme  27884  pntlem3  27885  pntlemp  27886  pntleml  27887  pnt3  27888  madebdaylemlrcut  28204  noinds  28250  no2indlesm  28259  no3inds  28263  precsexlem9  28520  istrkgld  28840  trgcgrg  28897  tgcgr4  28913  isperp  29106  brbtwn  29396  usgruspgrb  29683  nbgr2vtx1edg  29850  nbuhgr2vtx1edgb  29852  nbgr1vtx  29858  uvtx01vtx  29897  cplgr1v  29930  wlkeq  30133  wlkl1loop  30137  uspgr2wlkeq  30145  upgr2wlk  30166  redwlk  30170  wlkp1lem8  30178  usgr2wlkneq  30261  usgr2trlncl  30265  usgr2pthlem  30268  usgr2pth  30269  pthdlem1  30271  uspgrn2crct  30316  crctcshwlkn0  30329  wwlknp  30351  wwlksn0s  30369  wlkiswwlks1  30375  wlkiswwlks2lem4  30380  wwlksnred  30400  rusgrnumwwlkl1  30479  clwwlkccatlem  30499  clwlkclwwlklem2a1  30502  clwlkclwwlklem2a  30508  clwlkclwwlklem3  30511  clwwlkn  30536  clwwlknp  30547  clwwlkinwwlk  30550  clwwlkn1  30551  clwwlkn2  30554  clwwlkel  30556  clwwlkf  30557  clwwlkwwlksb  30564  1ewlk  30625  upgr3v3e3cycl  30700  upgr4cycl4dv4e  30705  dfconngr1  30708  isconngr1  30710  frgr3v  30795  frgrwopregasn  30836  frgrwopregbsn  30837  ubth  31394  acunirnmpt2  33173  acunirnmpt2f  33174  aciunf1  33176  fnpreimac  33183  fxpgaval  33647  crngmxidl  33913  lmxrge0  34503  measval  34750  isrnmeas  34752  sitgval  34884  eulerpartlemo  34917  eulerpartlemn  34933  onvf1odlem4  35804  subfacp1lem3  35862  subfacp1lem5  35864  txpconn  35912  cvxpconn  35922  cvmscbv  35938  cvmsi  35945  cvmsval  35946  satf  36033  sat1el2xp  36059  elmrsubrn  36200  weiunlem  37167  bj-raldifsn  37935  poimirlem26  38478  poimirlem27  38479  poimirlem31  38483  poimirlem32  38484  heicant  38487  mblfinlem3  38491  ovoliunnfl  38494  voliunnfl  38496  volsupnfl  38497  sdclem1  38591  fdc  38593  rrncmslem  38680  isass  38694  isrngod  38746  isgrpda  38803  iscom2  38843  pautsetN  41069  tendofset  41729  tendoset  41730  hdmap14lem13  42851  3factsumint1  42985  sticksstones3  43112  kelac1  44002  gicabl  44038  cantnfresb  44263  safesnsupfilb  44356  fiinfi  44511  clsk1independent  44984  wessf1ornlem  46115  uzub  46357  rexanuz2nf  46418  mccl  46526  climsuse  46536  limsupmnfuzlem  46652  limsupmnfuz  46653  limsupre3uzlem  46661  limsupre3uz  46662  limsupreuz  46663  0cnv  46668  climuz  46670  lmbr3  46673  limsupgt  46704  liminflt  46731  xlimpnfxnegmnf  46740  xlimmnf  46767  xlimpnf  46768  xlimmnfmpt  46769  xlimpnfmpt  46770  dfxlim2  46774  fourierdlem2  47035  fourierdlem3  47036  fourierdlem31  47064  fourierdlem47  47079  fourierdlem70  47102  fourierdlem71  47103  fourierdlem80  47112  fourierdlem103  47135  fourierdlem104  47136  fourierdlem113  47145  etransclem48  47208  etransc  47209  caragenval  47419  omessle  47424  smfmullem2  47718  smfmul  47721  2ffzoeq  48314  iccpval  48413  iccpartigtl  48421  nprmmul1  48525  cycl3grtrilem  48960  grlimedgclnbgr  49009  grlimgrtri  49017  grilcbri2  49025  usgrexmpl2trifr  49051  gpg5nbgrvtx03star  49094  gpg5nbgr3star  49095  lindsrng01  49496  rrx2line  49768  initopropd  50267  termopropd  50268  fucofulem2  50335  thincpropd  50466  isinito2lem  50522