Theorem raleqdv 3326

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ral 3063  df-rex 3072

This theorem is referenced by:  raleqbidva  3328  raleleqALT  3342  raldifeq  4494  frpoinsg  6345  wfisgOLD  6356  fveqressseq  7082  f12dfv  7271  f13dfv  7272  cbvfo  7287  isoselem  7338  ofrfvalg  7678  omsinds  7876  omsindsOLD  7877  frpoins3xpg  8126  frpoins3xp3g  8127  frrlem4  8274  wfrlem4OLD  8312  issmo2  8349  smoeq  8350  on2ind  8668  on3ind  8669  frfi  9288  marypha1lem  9428  marypha1  9429  dfoi  9506  oieq2  9508  ordtypecbv  9512  ordtypelem2  9514  ordtypelem3  9515  ordtypelem9  9521  wemapwe  9692  ttrclss  9715  ttrclselem2  9721  frinsg  9746  tcrank  9879  isacn  10039  pwsdompw  10199  isfin2  10289  isfin3ds  10324  isf33lem  10361  hsmexlem4  10424  zorn2lem6  10496  zorn2lem7  10497  zorn2g  10498  fpwwe2lem12  10637  uzsupss  12924  fzrevral2  13587  fzrevral3  13588  fzshftral  13589  fzoshftral  13749  uzsinds  13952  expmulnbnd  14198  eqs1  14562  swrdspsleq  14615  pfxeq  14646  pfxsuffeqwrdeq  14648  repswsymballbi  14730  cshw1  14772  pfx2  14898  wwlktovf1  14908  eqwrds3  14912  rexuz3  15295  rexuzre  15299  limsupgle  15421  rlim  15439  climconst  15487  rlimclim1  15489  climshftlem  15518  isercoll  15614  caucvgb  15626  serf0  15627  mertenslem1  15830  coprmprod  16598  coprmproddvds  16600  prmind2  16622  vdwlem10  16923  vdwlem13  16926  vdwnnlem2  16929  vdwnnlem3  16930  vdwnn  16931  ramval  16941  ramz  16958  prmgaplem5  16988  isacs  17595  cidpropd  17654  monpropd  17684  isssc  17767  fullsubc  17800  funcpropd  17851  isfth  17865  fthpropd  17872  grpidpropd  18581  sgrppropd  18622  mndpropd  18650  nmznsg  19048  ghmnsgima  19116  symgextfo  19290  gsmsymgrfixlem1  19295  gsmsymgrfix  19296  fvcosymgeq  19297  gsmsymgreqlem2  19299  symgfixf1  19305  psgnunilem3  19364  subgpgp  19465  sylow2blem3  19490  sylow3lem6  19500  efgsp1  19605  efgsres  19606  cmnpropd  19659  telgsumfzs  19857  ablfac2  19959  ringpropd  20102  abvpropd  20450  lsspropd  20628  lmhmpropd  20684  lbspropd  20710  pj1lmhm  20711  znf1o  21107  psgndiflemB  21153  phlpropd  21208  islindf  21367  lindfmm  21382  islindf4  21393  islindf5  21394  assapropd  21426  scmatf1  22033  isclo  22591  perfopn  22689  lmfval  22736  lmconst  22765  cncnp  22784  iscnrm2  22842  ist0-2  22848  ist1-2  22851  ishaus2  22855  ordtt1  22883  subislly  22985  elpt  23076  elptr  23077  ptbasfi  23085  tx1stc  23154  xkococnlem  23163  fclscmp  23534  ufilcmp  23536  cnpfcf  23545  alexsubALTlem1  23551  alexsubALTlem2  23552  alexsubALTlem4  23554  tmdgsum2  23600  tsmsf1o  23649  ustval  23707  ucnval  23782  imasdsf1olem  23879  imasf1oxmet  23881  imasf1omet  23882  metss  24017  prdsxmslem2  24038  cnmpopc  24444  lebnumlem3  24479  ishtpy  24488  pi1coghm  24577  lmnn  24780  evthicc  24976  cniccbdd  24978  ovolicc2lem4  25037  0pledm  25190  cniccibl  25358  cnicciblnc  25360  c1lip1  25514  dvivthlem1  25525  lhop1  25531  itgsubstlem  25565  dgrlem  25743  ulmshftlem  25901  ulm0  25903  ulmcau  25907  iblulm  25919  rlimcnp  26470  xrlimcnp  26473  fsumdvdsmul  26699  chtub  26715  2sqlem10  26931  dchrisum0flb  27013  pntpbnd1  27089  pntpbnd  27091  pntibndlem2  27094  pntibndlem3  27095  pntibnd  27096  pntlemi  27107  pntleme  27111  pntlem3  27112  pntlemp  27113  pntleml  27114  pnt3  27115  madebdaylemlrcut  27393  noinds  27429  no2indslem  27438  no3inds  27442  precsexlem9  27661  istrkgld  27710  trgcgrg  27766  tgcgr4  27782  isperp  27963  brbtwn  28157  usgruspgrb  28441  usgr1e  28502  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  nbgr0vtx  28613  nbgr1vtx  28615  uvtx01vtx  28654  cplgr1v  28687  cusgrexi  28700  1hevtxdg0  28762  wlkeq  28891  wlkl1loop  28895  uspgr2wlkeq  28903  upgr2wlk  28925  redwlk  28929  wlkp1lem8  28937  usgr2wlkneq  29013  usgr2trlncl  29017  usgr2pthlem  29020  usgr2pth  29021  pthdlem1  29023  uspgrn2crct  29062  crctcshwlkn0lem7  29070  crctcshwlkn0  29075  wwlknp  29097  wwlksn0s  29115  wlkiswwlks1  29121  wlkiswwlks2lem4  29126  wlkiswwlksupgr2  29131  wlknewwlksn  29141  wwlksnred  29146  wwlksnext  29147  rusgrnumwwlkl1  29222  clwwlkccatlem  29242  clwlkclwwlklem2a1  29245  clwlkclwwlklem2a  29251  clwlkclwwlklem3  29254  clwlkclwwlkf1lem3  29259  clwwlkn  29279  clwwlknp  29290  clwwlkinwwlk  29293  clwwlkn1  29294  clwwlkn2  29297  clwwlkel  29299  clwwlkf  29300  clwwlkwwlksb  29307  wwlksext2clwwlk  29310  wwlksubclwwlk  29311  clwwlknonex2  29362  1ewlk  29368  1wlkdlem4  29393  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  dfconngr1  29441  isconngr1  29443  frgr3v  29528  frgrwopregasn  29569  frgrwopregbsn  29570  ubth  30126  acunirnmpt2  31885  acunirnmpt2f  31886  aciunf1  31888  fnpreimac  31896  crngmxidl  32585  lmxrge0  32932  sigaclcu3  33120  measval  33196  isrnmeas  33198  sitgval  33331  eulerpartlemsv3  33360  eulerpartlemo  33364  eulerpartlemn  33380  bnj1514  34074  subfacp1lem3  34173  subfacp1lem5  34175  txpconn  34223  cvxpconn  34233  cvmscbv  34249  cvmsi  34256  cvmsval  34257  satf  34344  sat1el2xp  34370  elmrsubrn  34511  bj-raldifsn  35981  poimirlem1  36489  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  poimirlem32  36520  heicant  36523  mblfinlem3  36527  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  sdclem1  36611  fdc  36613  rrncmslem  36700  isass  36714  exidreslem  36745  exidresid  36747  isrngod  36766  isgrpda  36823  iscom2  36863  pautsetN  38969  tendofset  39629  tendoset  39630  hdmap14lem13  40751  3factsumint1  40886  sticksstones3  40964  kelac1  41805  gicabl  41841  lpirlnr  41859  cantnfresb  42074  oaun3lem1  42124  naddsuc2  42143  safesnsupfilb  42169  fiinfi  42324  clsk1independent  42797  scotteqd  42996  wessf1ornlem  43882  uzub  44141  rexanuz2nf  44203  mccl  44314  climsuse  44324  limsupmnfuzlem  44442  limsupmnfuz  44443  limsupre3uzlem  44451  limsupre3uz  44452  limsupreuz  44453  0cnv  44458  climuz  44460  lmbr3  44463  limsupgt  44494  liminflt  44521  xlimpnfxnegmnf  44530  xlimmnf  44557  xlimpnf  44558  xlimmnfmpt  44559  xlimpnfmpt  44560  dfxlim2  44564  fourierdlem2  44825  fourierdlem3  44826  fourierdlem31  44854  fourierdlem47  44869  fourierdlem70  44892  fourierdlem71  44893  fourierdlem73  44895  fourierdlem80  44902  fourierdlem103  44925  fourierdlem104  44926  fourierdlem113  44935  etransclem48  44998  etransc  44999  caragenval  45209  omessle  45214  smfmullem2  45508  smfmul  45511  2ffzoeq  46036  iccpval  46083  iccpartigtl  46091  rngpropd  46673  c0snmgmhm  46713  linds0  47146  lindsrng01  47149  rrx2line  47426