Theorem raleqdv 3323

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∀wral 3059

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ral 3060  df-rex 3069

This theorem is referenced by:  raleqbidva  3325  raleleqALT  3339  raldifeq  4492  frpoinsg  6343  wfisgOLD  6354  fveqressseq  7080  f12dfv  7273  f13dfv  7274  cbvfo  7289  isoselem  7340  ofrfvalg  7680  omsinds  7878  omsindsOLD  7879  frpoins3xpg  8128  frpoins3xp3g  8129  frrlem4  8276  wfrlem4OLD  8314  issmo2  8351  smoeq  8352  on2ind  8670  on3ind  8671  frfi  9290  marypha1lem  9430  marypha1  9431  dfoi  9508  oieq2  9510  ordtypecbv  9514  ordtypelem2  9516  ordtypelem3  9517  ordtypelem9  9523  wemapwe  9694  ttrclss  9717  ttrclselem2  9723  frinsg  9748  tcrank  9881  isacn  10041  pwsdompw  10201  isfin2  10291  isfin3ds  10326  isf33lem  10363  hsmexlem4  10426  zorn2lem6  10498  zorn2lem7  10499  zorn2g  10500  fpwwe2lem12  10639  uzsupss  12928  fzrevral2  13591  fzrevral3  13592  fzshftral  13593  fzoshftral  13753  uzsinds  13956  expmulnbnd  14202  eqs1  14566  swrdspsleq  14619  pfxeq  14650  pfxsuffeqwrdeq  14652  repswsymballbi  14734  cshw1  14776  pfx2  14902  wwlktovf1  14912  eqwrds3  14916  rexuz3  15299  rexuzre  15303  limsupgle  15425  rlim  15443  climconst  15491  rlimclim1  15493  climshftlem  15522  isercoll  15618  caucvgb  15630  serf0  15631  mertenslem1  15834  coprmprod  16602  coprmproddvds  16604  prmind2  16626  vdwlem10  16927  vdwlem13  16930  vdwnnlem2  16933  vdwnnlem3  16934  vdwnn  16935  ramval  16945  ramz  16962  prmgaplem5  16992  isacs  17599  cidpropd  17658  monpropd  17688  isssc  17771  fullsubc  17804  funcpropd  17855  isfth  17869  fthpropd  17876  grpidpropd  18587  sgrppropd  18656  mndpropd  18684  nmznsg  19084  ghmnsgima  19154  symgextfo  19331  gsmsymgrfixlem1  19336  gsmsymgrfix  19337  fvcosymgeq  19338  gsmsymgreqlem2  19340  symgfixf1  19346  psgnunilem3  19405  subgpgp  19506  sylow2blem3  19531  sylow3lem6  19541  efgsp1  19646  efgsres  19647  cmnpropd  19700  telgsumfzs  19898  ablfac2  20000  rngpropd  20068  ringpropd  20176  c0snmgmhm  20353  abvpropd  20593  lsspropd  20772  lmhmpropd  20828  lbspropd  20854  pj1lmhm  20855  znf1o  21326  psgndiflemB  21372  phlpropd  21427  islindf  21586  lindfmm  21601  islindf4  21612  islindf5  21613  assapropd  21645  scmatf1  22253  isclo  22811  perfopn  22909  lmfval  22956  lmconst  22985  cncnp  23004  iscnrm2  23062  ist0-2  23068  ist1-2  23071  ishaus2  23075  ordtt1  23103  subislly  23205  elpt  23296  elptr  23297  ptbasfi  23305  tx1stc  23374  xkococnlem  23383  fclscmp  23754  ufilcmp  23756  cnpfcf  23765  alexsubALTlem1  23771  alexsubALTlem2  23772  alexsubALTlem4  23774  tmdgsum2  23820  tsmsf1o  23869  ustval  23927  ucnval  24002  imasdsf1olem  24099  imasf1oxmet  24101  imasf1omet  24102  metss  24237  prdsxmslem2  24258  cnmpopc  24669  lebnumlem3  24709  ishtpy  24718  pi1coghm  24808  lmnn  25011  evthicc  25208  cniccbdd  25210  ovolicc2lem4  25269  0pledm  25422  cniccibl  25590  cnicciblnc  25592  c1lip1  25749  dvivthlem1  25760  lhop1  25766  itgsubstlem  25800  dgrlem  25978  ulmshftlem  26137  ulm0  26139  ulmcau  26143  iblulm  26155  rlimcnp  26706  xrlimcnp  26709  fsumdvdsmul  26935  chtub  26951  2sqlem10  27167  dchrisum0flb  27249  pntpbnd1  27325  pntpbnd  27327  pntibndlem2  27330  pntibndlem3  27331  pntibnd  27332  pntlemi  27343  pntleme  27347  pntlem3  27348  pntlemp  27349  pntleml  27350  pnt3  27351  madebdaylemlrcut  27630  noinds  27667  no2indslem  27676  no3inds  27680  precsexlem9  27900  istrkgld  27977  trgcgrg  28033  tgcgr4  28049  isperp  28230  brbtwn  28424  usgruspgrb  28708  usgr1e  28769  nbgr2vtx1edg  28874  nbuhgr2vtx1edgb  28876  nbgr0vtx  28880  nbgr1vtx  28882  uvtx01vtx  28921  cplgr1v  28954  cusgrexi  28967  1hevtxdg0  29029  wlkeq  29158  wlkl1loop  29162  uspgr2wlkeq  29170  upgr2wlk  29192  redwlk  29196  wlkp1lem8  29204  usgr2wlkneq  29280  usgr2trlncl  29284  usgr2pthlem  29287  usgr2pth  29288  pthdlem1  29290  uspgrn2crct  29329  crctcshwlkn0lem7  29337  crctcshwlkn0  29342  wwlknp  29364  wwlksn0s  29382  wlkiswwlks1  29388  wlkiswwlks2lem4  29393  wlkiswwlksupgr2  29398  wlknewwlksn  29408  wwlksnred  29413  wwlksnext  29414  rusgrnumwwlkl1  29489  clwwlkccatlem  29509  clwlkclwwlklem2a1  29512  clwlkclwwlklem2a  29518  clwlkclwwlklem3  29521  clwlkclwwlkf1lem3  29526  clwwlkn  29546  clwwlknp  29557  clwwlkinwwlk  29560  clwwlkn1  29561  clwwlkn2  29564  clwwlkel  29566  clwwlkf  29567  clwwlkwwlksb  29574  wwlksext2clwwlk  29577  wwlksubclwwlk  29578  clwwlknonex2  29629  1ewlk  29635  1wlkdlem4  29660  upgr3v3e3cycl  29700  upgr4cycl4dv4e  29705  dfconngr1  29708  isconngr1  29710  frgr3v  29795  frgrwopregasn  29836  frgrwopregbsn  29837  ubth  30393  acunirnmpt2  32152  acunirnmpt2f  32153  aciunf1  32155  fnpreimac  32163  crngmxidl  32859  lmxrge0  33230  sigaclcu3  33418  measval  33494  isrnmeas  33496  sitgval  33629  eulerpartlemsv3  33658  eulerpartlemo  33662  eulerpartlemn  33678  bnj1514  34372  subfacp1lem3  34471  subfacp1lem5  34473  txpconn  34521  cvxpconn  34531  cvmscbv  34547  cvmsi  34554  cvmsval  34555  satf  34642  sat1el2xp  34668  elmrsubrn  34809  bj-raldifsn  36284  poimirlem1  36792  poimirlem26  36817  poimirlem27  36818  poimirlem31  36822  poimirlem32  36823  heicant  36826  mblfinlem3  36830  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  sdclem1  36914  fdc  36916  rrncmslem  37003  isass  37017  exidreslem  37048  exidresid  37050  isrngod  37069  isgrpda  37126  iscom2  37166  pautsetN  39272  tendofset  39932  tendoset  39933  hdmap14lem13  41054  3factsumint1  41192  sticksstones3  41270  kelac1  42107  gicabl  42143  lpirlnr  42161  cantnfresb  42376  oaun3lem1  42426  naddsuc2  42445  safesnsupfilb  42471  fiinfi  42626  clsk1independent  43099  scotteqd  43298  wessf1ornlem  44182  uzub  44439  rexanuz2nf  44501  mccl  44612  climsuse  44622  limsupmnfuzlem  44740  limsupmnfuz  44741  limsupre3uzlem  44749  limsupre3uz  44750  limsupreuz  44751  0cnv  44756  climuz  44758  lmbr3  44761  limsupgt  44792  liminflt  44819  xlimpnfxnegmnf  44828  xlimmnf  44855  xlimpnf  44856  xlimmnfmpt  44857  xlimpnfmpt  44858  dfxlim2  44862  fourierdlem2  45123  fourierdlem3  45124  fourierdlem31  45152  fourierdlem47  45167  fourierdlem70  45190  fourierdlem71  45191  fourierdlem73  45193  fourierdlem80  45200  fourierdlem103  45223  fourierdlem104  45224  fourierdlem113  45233  etransclem48  45296  etransc  45297  caragenval  45507  omessle  45512  smfmullem2  45806  smfmul  45809  2ffzoeq  46334  iccpval  46381  iccpartigtl  46389  linds0  47233  lindsrng01  47236  rrx2line  47513