Theorem raleqdv 3364

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)

Hypothesis

Ref	Expression
raleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
raleqdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		raleq 3358	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111

This theorem is referenced by:  raleqbidva  3370  raleleqALT  3373  raldifeq  4397  wfisg  6151  fveqressseq  6824  f12dfv  7008  f13dfv  7009  cbvfo  7023  isoselem  7073  ofrfval  7397  omsinds  7580  wfrlem4  7941  issmo2  7969  smoeq  7970  frfi  8747  marypha1lem  8881  marypha1  8882  dfoi  8959  oieq2  8961  ordtypecbv  8965  ordtypelem2  8967  ordtypelem3  8968  ordtypelem9  8974  wemapwe  9144  tcrank  9297  isacn  9455  pwsdompw  9615  isfin2  9705  isfin3ds  9740  isf33lem  9777  hsmexlem4  9840  zorn2lem6  9912  zorn2lem7  9913  zorn2g  9914  fpwwe2lem13  10053  uzsupss  12328  fzrevral2  12988  fzrevral3  12989  fzshftral  12990  fzoshftral  13149  uzsinds  13350  expmulnbnd  13592  eqs1  13957  swrdspsleq  14018  pfxeq  14049  pfxsuffeqwrdeq  14051  repswsymballbi  14133  cshw1  14175  pfx2  14300  wwlktovf1  14312  eqwrds3  14316  rexuz3  14700  rexuzre  14704  limsupgle  14826  rlim  14844  climconst  14892  rlimclim1  14894  climshftlem  14923  isercoll  15016  caucvgb  15028  serf0  15029  mertenslem1  15232  coprmprod  15995  coprmproddvds  15997  prmind2  16019  vdwlem10  16316  vdwlem13  16319  vdwnnlem2  16322  vdwnnlem3  16323  vdwnn  16324  ramval  16334  ramz  16351  prmgaplem5  16381  isacs  16914  cidpropd  16972  monpropd  16999  isssc  17082  fullsubc  17112  funcpropd  17162  isfth  17176  fthpropd  17183  grpidpropd  17864  mndpropd  17928  nmznsg  18312  ghmnsgima  18374  symgextfo  18542  gsmsymgrfixlem1  18547  gsmsymgrfix  18548  fvcosymgeq  18549  gsmsymgreqlem2  18551  symgfixf1  18557  psgnunilem3  18616  subgpgp  18714  sylow2blem3  18739  sylow3lem6  18749  efgsp1  18855  efgsres  18856  cmnpropd  18908  telgsumfzs  19102  ablfac2  19204  ringpropd  19328  abvpropd  19606  lsspropd  19782  lmhmpropd  19838  lbspropd  19864  pj1lmhm  19865  znf1o  20243  psgndiflemB  20289  phlpropd  20344  islindf  20501  lindfmm  20516  islindf4  20527  islindf5  20528  assapropd  20558  scmatf1  21136  isclo  21692  perfopn  21790  lmfval  21837  lmconst  21866  cncnp  21885  iscnrm2  21943  ist0-2  21949  ist1-2  21952  ishaus2  21956  ordtt1  21984  subislly  22086  elpt  22177  elptr  22178  ptbasfi  22186  tx1stc  22255  xkococnlem  22264  fclscmp  22635  ufilcmp  22637  cnpfcf  22646  alexsubALTlem1  22652  alexsubALTlem2  22653  alexsubALTlem4  22655  tmdgsum2  22701  tsmsf1o  22750  ustval  22808  ucnval  22883  imasdsf1olem  22980  imasf1oxmet  22982  imasf1omet  22983  metss  23115  prdsxmslem2  23136  cnmpopc  23533  lebnumlem3  23568  ishtpy  23577  pi1coghm  23666  lmnn  23867  evthicc  24063  cniccbdd  24065  ovolicc2lem4  24124  0pledm  24277  cniccibl  24444  cnicciblnc  24446  c1lip1  24600  dvivthlem1  24611  lhop1  24617  itgsubstlem  24651  dgrlem  24826  ulmshftlem  24984  ulm0  24986  ulmcau  24990  iblulm  25002  rlimcnp  25551  xrlimcnp  25554  fsumdvdsmul  25780  chtub  25796  2sqlem10  26012  dchrisum0flb  26094  pntpbnd1  26170  pntpbnd  26172  pntibndlem2  26175  pntibndlem3  26176  pntibnd  26177  pntlemi  26188  pntleme  26192  pntlem3  26193  pntlemp  26194  pntleml  26195  pnt3  26196  istrkgld  26253  trgcgrg  26309  tgcgr4  26325  isperp  26506  brbtwn  26693  usgruspgrb  26974  usgr1e  27035  nbgr2vtx1edg  27140  nbuhgr2vtx1edgb  27142  nbgr0vtx  27146  nbgr1vtx  27148  uvtx01vtx  27187  cplgr1v  27220  cusgrexi  27233  1hevtxdg0  27295  wlkeq  27423  wlkl1loop  27427  uspgr2wlkeq  27435  upgr2wlk  27458  redwlk  27462  wlkp1lem8  27470  usgr2wlkneq  27545  usgr2trlncl  27549  usgr2pthlem  27552  usgr2pth  27553  pthdlem1  27555  uspgrn2crct  27594  crctcshwlkn0lem7  27602  crctcshwlkn0  27607  wwlknp  27629  wwlksn0s  27647  wlkiswwlks1  27653  wlkiswwlks2lem4  27658  wlkiswwlksupgr2  27663  wlknewwlksn  27673  wwlksnred  27678  wwlksnext  27679  rusgrnumwwlkl1  27754  clwwlkccatlem  27774  clwlkclwwlklem2a1  27777  clwlkclwwlklem2a  27783  clwlkclwwlklem3  27786  clwlkclwwlkf1lem3  27791  clwwlkn  27811  clwwlknp  27822  clwwlkinwwlk  27825  clwwlkn1  27826  clwwlkn2  27829  clwwlkel  27831  clwwlkf  27832  clwwlkwwlksb  27839  wwlksext2clwwlk  27842  wwlksubclwwlk  27843  clwwlknonex2  27894  1ewlk  27900  1wlkdlem4  27925  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  dfconngr1  27973  isconngr1  27975  frgr3v  28060  frgrwopregasn  28101  frgrwopregbsn  28102  ubth  28656  acunirnmpt2  30423  acunirnmpt2f  30424  aciunf1  30426  fnpreimac  30434  lmxrge0  31305  sigaclcu3  31491  measval  31567  isrnmeas  31569  sitgval  31700  eulerpartlemsv3  31729  eulerpartlemo  31733  eulerpartlemn  31749  bnj1514  32445  subfacp1lem3  32542  subfacp1lem5  32544  txpconn  32592  cvxpconn  32602  cvmscbv  32618  cvmsi  32625  cvmsval  32626  satf  32713  sat1el2xp  32739  elmrsubrn  32880  frpoinsg  33194  frinsg  33200  frrlem4  33239  bj-raldifsn  34515  poimirlem1  35058  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  poimirlem32  35089  heicant  35092  mblfinlem3  35096  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  sdclem1  35181  fdc  35183  rrncmslem  35270  isass  35284  exidreslem  35315  exidresid  35317  isrngod  35336  isgrpda  35393  iscom2  35433  pautsetN  37394  tendofset  38054  tendoset  38055  hdmap14lem13  39176  3factsumint1  39309  kelac1  40007  gicabl  40043  lpirlnr  40061  fiinfi  40272  clsk1independent  40749  scotteqd  40945  wessf1ornlem  41811  uzub  42068  mccl  42240  climsuse  42250  limsupmnfuzlem  42368  limsupmnfuz  42369  limsupre3uzlem  42377  limsupre3uz  42378  limsupreuz  42379  0cnv  42384  climuz  42386  lmbr3  42389  limsupgt  42420  liminflt  42447  xlimpnfxnegmnf  42456  xlimmnf  42483  xlimpnf  42484  xlimmnfmpt  42485  xlimpnfmpt  42486  dfxlim2  42490  fourierdlem2  42751  fourierdlem3  42752  fourierdlem31  42780  fourierdlem47  42795  fourierdlem70  42818  fourierdlem71  42819  fourierdlem73  42821  fourierdlem80  42828  fourierdlem103  42851  fourierdlem104  42852  fourierdlem113  42861  etransclem48  42924  etransc  42925  caragenval  43132  omessle  43137  smfmullem2  43424  smfmul  43427  2ffzoeq  43885  iccpval  43932  iccpartigtl  43940  c0snmgmhm  44538  linds0  44874  lindsrng01  44877  rrx2line  45154