Theorem raleqdv 3325

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ral 3062  df-rex 3071

This theorem is referenced by:  raleqbidva  3327  raleleqALT  3341  raldifeq  4488  frpoinsg  6334  wfisgOLD  6345  fveqressseq  7067  f12dfv  7256  f13dfv  7257  cbvfo  7272  isoselem  7323  ofrfvalg  7662  omsinds  7860  omsindsOLD  7861  frpoins3xpg  8110  frpoins3xp3g  8111  frrlem4  8258  wfrlem4OLD  8296  issmo2  8333  smoeq  8334  on2ind  8653  on3ind  8654  frfi  9273  marypha1lem  9412  marypha1  9413  dfoi  9490  oieq2  9492  ordtypecbv  9496  ordtypelem2  9498  ordtypelem3  9499  ordtypelem9  9505  wemapwe  9676  ttrclss  9699  ttrclselem2  9705  frinsg  9730  tcrank  9863  isacn  10023  pwsdompw  10183  isfin2  10273  isfin3ds  10308  isf33lem  10345  hsmexlem4  10408  zorn2lem6  10480  zorn2lem7  10481  zorn2g  10482  fpwwe2lem12  10621  uzsupss  12908  fzrevral2  13571  fzrevral3  13572  fzshftral  13573  fzoshftral  13733  uzsinds  13936  expmulnbnd  14182  eqs1  14546  swrdspsleq  14599  pfxeq  14630  pfxsuffeqwrdeq  14632  repswsymballbi  14714  cshw1  14756  pfx2  14882  wwlktovf1  14892  eqwrds3  14896  rexuz3  15279  rexuzre  15283  limsupgle  15405  rlim  15423  climconst  15471  rlimclim1  15473  climshftlem  15502  isercoll  15598  caucvgb  15610  serf0  15611  mertenslem1  15814  coprmprod  16582  coprmproddvds  16584  prmind2  16606  vdwlem10  16907  vdwlem13  16910  vdwnnlem2  16913  vdwnnlem3  16914  vdwnn  16915  ramval  16925  ramz  16942  prmgaplem5  16972  isacs  17579  cidpropd  17638  monpropd  17668  isssc  17751  fullsubc  17784  funcpropd  17835  isfth  17849  fthpropd  17856  grpidpropd  18565  mndpropd  18629  nmznsg  19022  ghmnsgima  19084  symgextfo  19256  gsmsymgrfixlem1  19261  gsmsymgrfix  19262  fvcosymgeq  19263  gsmsymgreqlem2  19265  symgfixf1  19271  psgnunilem3  19330  subgpgp  19431  sylow2blem3  19456  sylow3lem6  19466  efgsp1  19571  efgsres  19572  cmnpropd  19625  telgsumfzs  19818  ablfac2  19920  ringpropd  20061  abvpropd  20401  lsspropd  20579  lmhmpropd  20635  lbspropd  20661  pj1lmhm  20662  znf1o  21042  psgndiflemB  21088  phlpropd  21143  islindf  21302  lindfmm  21317  islindf4  21328  islindf5  21329  assapropd  21359  scmatf1  21964  isclo  22522  perfopn  22620  lmfval  22667  lmconst  22696  cncnp  22715  iscnrm2  22773  ist0-2  22779  ist1-2  22782  ishaus2  22786  ordtt1  22814  subislly  22916  elpt  23007  elptr  23008  ptbasfi  23016  tx1stc  23085  xkococnlem  23094  fclscmp  23465  ufilcmp  23467  cnpfcf  23476  alexsubALTlem1  23482  alexsubALTlem2  23483  alexsubALTlem4  23485  tmdgsum2  23531  tsmsf1o  23580  ustval  23638  ucnval  23713  imasdsf1olem  23810  imasf1oxmet  23812  imasf1omet  23813  metss  23948  prdsxmslem2  23969  cnmpopc  24375  lebnumlem3  24410  ishtpy  24419  pi1coghm  24508  lmnn  24711  evthicc  24907  cniccbdd  24909  ovolicc2lem4  24968  0pledm  25121  cniccibl  25289  cnicciblnc  25291  c1lip1  25445  dvivthlem1  25456  lhop1  25462  itgsubstlem  25496  dgrlem  25674  ulmshftlem  25832  ulm0  25834  ulmcau  25838  iblulm  25850  rlimcnp  26399  xrlimcnp  26402  fsumdvdsmul  26628  chtub  26644  2sqlem10  26860  dchrisum0flb  26942  pntpbnd1  27018  pntpbnd  27020  pntibndlem2  27023  pntibndlem3  27024  pntibnd  27025  pntlemi  27036  pntleme  27040  pntlem3  27041  pntlemp  27042  pntleml  27043  pnt3  27044  madebdaylemlrcut  27322  noinds  27358  no2indslem  27367  no3inds  27371  precsexlem9  27590  istrkgld  27639  trgcgrg  27695  tgcgr4  27711  isperp  27892  brbtwn  28086  usgruspgrb  28370  usgr1e  28431  nbgr2vtx1edg  28536  nbuhgr2vtx1edgb  28538  nbgr0vtx  28542  nbgr1vtx  28544  uvtx01vtx  28583  cplgr1v  28616  cusgrexi  28629  1hevtxdg0  28691  wlkeq  28820  wlkl1loop  28824  uspgr2wlkeq  28832  upgr2wlk  28854  redwlk  28858  wlkp1lem8  28866  usgr2wlkneq  28942  usgr2trlncl  28946  usgr2pthlem  28949  usgr2pth  28950  pthdlem1  28952  uspgrn2crct  28991  crctcshwlkn0lem7  28999  crctcshwlkn0  29004  wwlknp  29026  wwlksn0s  29044  wlkiswwlks1  29050  wlkiswwlks2lem4  29055  wlkiswwlksupgr2  29060  wlknewwlksn  29070  wwlksnred  29075  wwlksnext  29076  rusgrnumwwlkl1  29151  clwwlkccatlem  29171  clwlkclwwlklem2a1  29174  clwlkclwwlklem2a  29180  clwlkclwwlklem3  29183  clwlkclwwlkf1lem3  29188  clwwlkn  29208  clwwlknp  29219  clwwlkinwwlk  29222  clwwlkn1  29223  clwwlkn2  29226  clwwlkel  29228  clwwlkf  29229  clwwlkwwlksb  29236  wwlksext2clwwlk  29239  wwlksubclwwlk  29240  clwwlknonex2  29291  1ewlk  29297  1wlkdlem4  29322  upgr3v3e3cycl  29362  upgr4cycl4dv4e  29367  dfconngr1  29370  isconngr1  29372  frgr3v  29457  frgrwopregasn  29498  frgrwopregbsn  29499  ubth  30053  acunirnmpt2  31818  acunirnmpt2f  31819  aciunf1  31821  fnpreimac  31829  crngmxidl  32500  lmxrge0  32827  sigaclcu3  33015  measval  33091  isrnmeas  33093  sitgval  33226  eulerpartlemsv3  33255  eulerpartlemo  33259  eulerpartlemn  33275  bnj1514  33969  subfacp1lem3  34068  subfacp1lem5  34070  txpconn  34118  cvxpconn  34128  cvmscbv  34144  cvmsi  34151  cvmsval  34152  satf  34239  sat1el2xp  34265  elmrsubrn  34406  bj-raldifsn  35849  poimirlem1  36357  poimirlem26  36382  poimirlem27  36383  poimirlem31  36387  poimirlem32  36388  heicant  36391  mblfinlem3  36395  ovoliunnfl  36398  voliunnfl  36400  volsupnfl  36401  sdclem1  36480  fdc  36482  rrncmslem  36569  isass  36583  exidreslem  36614  exidresid  36616  isrngod  36635  isgrpda  36692  iscom2  36732  pautsetN  38838  tendofset  39498  tendoset  39499  hdmap14lem13  40620  3factsumint1  40755  sticksstones3  40833  kelac1  41640  gicabl  41676  lpirlnr  41694  cantnfresb  41909  oaun3lem1  41959  naddsuc2  41978  safesnsupfilb  42004  fiinfi  42159  clsk1independent  42632  scotteqd  42831  wessf1ornlem  43717  uzub  43978  rexanuz2nf  44040  mccl  44151  climsuse  44161  limsupmnfuzlem  44279  limsupmnfuz  44280  limsupre3uzlem  44288  limsupre3uz  44289  limsupreuz  44290  0cnv  44295  climuz  44297  lmbr3  44300  limsupgt  44331  liminflt  44358  xlimpnfxnegmnf  44367  xlimmnf  44394  xlimpnf  44395  xlimmnfmpt  44396  xlimpnfmpt  44397  dfxlim2  44401  fourierdlem2  44662  fourierdlem3  44663  fourierdlem31  44691  fourierdlem47  44706  fourierdlem70  44729  fourierdlem71  44730  fourierdlem73  44732  fourierdlem80  44739  fourierdlem103  44762  fourierdlem104  44763  fourierdlem113  44772  etransclem48  44835  etransc  44836  caragenval  45046  omessle  45051  smfmullem2  45345  smfmul  45348  2ffzoeq  45872  iccpval  45919  iccpartigtl  45927  c0snmgmhm  46524  linds0  46858  lindsrng01  46861  rrx2line  47138