Theorem raleqdv 3296

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∀wral 3052

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ral 3053  df-rex 3063

This theorem is referenced by:  raleqtrdv  3298  raleqtrrdv  3300  raleqbidva  3302  raleleqOLD  3309  raldifeq  4434  frpoinsg  6303  f12dfv  7223  f13dfv  7224  cbvfo  7239  isoselem  7291  ofrfvalg  7634  omsinds  7833  frpoins3xpg  8085  frpoins3xp3g  8086  frrlem4  8234  issmo2  8284  smoeq  8285  on2ind  8600  on3ind  8601  naddsuc2  8632  frfi  9190  marypha1lem  9341  marypha1  9342  dfoi  9421  oieq2  9423  ordtypecbv  9427  ordtypelem2  9429  ordtypelem3  9430  ordtypelem9  9436  wemapwe  9613  ttrclss  9636  ttrclselem2  9642  frinsg  9670  tcrank  9803  isacn  9961  pwsdompw  10120  isfin2  10211  isfin3ds  10246  isf33lem  10283  hsmexlem4  10346  zorn2lem6  10418  zorn2lem7  10419  zorn2g  10420  fpwwe2lem12  10560  uzsupss  12885  fzrevral2  13562  fzrevral3  13563  fzshftral  13564  fzoshftral  13737  uzsinds  13944  expmulnbnd  14192  eqs1  14570  swrdspsleq  14623  pfxeq  14653  pfxsuffeqwrdeq  14655  repswsymballbi  14737  cshw1  14779  pfx2  14904  wwlktovf1  14914  eqwrds3  14918  rexuz3  15306  rexuzre  15310  limsupgle  15434  rlim  15452  climconst  15500  rlimclim1  15502  climshftlem  15531  isercoll  15625  caucvgb  15637  serf0  15638  mertenslem1  15844  coprmprod  16625  coprmproddvds  16627  prmind2  16649  vdwlem10  16956  vdwlem13  16959  vdwnnlem2  16962  vdwnnlem3  16963  vdwnn  16964  ramval  16974  ramz  16991  prmgaplem5  17021  isacs  17612  cidpropd  17671  monpropd  17699  isssc  17782  fullsubc  17812  funcpropd  17864  isfth  17878  fthpropd  17885  grpidpropd  18625  sgrppropd  18694  mndpropd  18722  nmznsg  19138  ghmnsgima  19210  symgextfo  19392  gsmsymgrfixlem1  19397  gsmsymgrfix  19398  fvcosymgeq  19399  gsmsymgreqlem2  19401  psgnunilem3  19466  sylow2blem3  19592  sylow3lem6  19602  cmnpropd  19761  telgsumfzs  19959  rngpropd  20150  ringpropd  20264  c0snmgmhm  20437  abvpropd  20807  lsspropd  21008  lmhmpropd  21064  lbspropd  21090  pj1lmhm  21091  psgndiflemB  21594  phlpropd  21649  islindf  21806  lindfmm  21821  islindf4  21832  islindf5  21833  assapropd  21865  scmatf1  22510  isclo  23066  lmfval  23211  lmconst  23240  iscnrm2  23317  ist0-2  23323  ist1-2  23326  ishaus2  23330  subislly  23460  elpt  23551  elptr  23552  ptbasfi  23560  fclscmp  24009  ufilcmp  24011  cnpfcf  24020  alexsubALTlem1  24026  alexsubALTlem2  24027  alexsubALTlem4  24029  tmdgsum2  24075  tsmsf1o  24124  ustval  24182  ucnval  24255  imasdsf1olem  24352  imasf1oxmet  24354  imasf1omet  24355  metss  24487  prdsxmslem2  24508  lebnumlem3  24944  ishtpy  24953  lmnn  25244  evthicc  25440  cniccbdd  25442  ovolicc2lem4  25501  0pledm  25654  cniccibl  25822  cnicciblnc  25824  c1lip1  25978  lhop1  25995  itgsubstlem  26029  ulmshftlem  26371  ulm0  26373  ulmcau  26377  rlimcnp  26946  fsumdvdsmul  27176  chtub  27193  2sqlem10  27409  dchrisum0flb  27491  pntpbnd1  27567  pntpbnd  27569  pntibndlem2  27572  pntibndlem3  27573  pntibnd  27574  pntlemi  27585  pntleme  27589  pntlem3  27590  pntlemp  27591  pntleml  27592  pnt3  27593  madebdaylemlrcut  27909  noinds  27955  no2indlesm  27964  no3inds  27968  precsexlem9  28225  istrkgld  28545  trgcgrg  28601  tgcgr4  28617  isperp  28798  brbtwn  28986  usgruspgrb  29270  nbgr2vtx1edg  29437  nbuhgr2vtx1edgb  29439  nbgr1vtx  29445  uvtx01vtx  29484  cplgr1v  29517  wlkeq  29721  wlkl1loop  29725  uspgr2wlkeq  29733  upgr2wlk  29754  redwlk  29758  wlkp1lem8  29766  usgr2wlkneq  29843  usgr2trlncl  29847  usgr2pthlem  29850  usgr2pth  29851  pthdlem1  29853  uspgrn2crct  29895  crctcshwlkn0  29908  wwlknp  29930  wwlksn0s  29948  wlkiswwlks1  29954  wlkiswwlks2lem4  29959  wwlksnred  29979  rusgrnumwwlkl1  30058  clwwlkccatlem  30078  clwlkclwwlklem2a1  30081  clwlkclwwlklem2a  30087  clwlkclwwlklem3  30090  clwwlkn  30115  clwwlknp  30126  clwwlkinwwlk  30129  clwwlkn1  30130  clwwlkn2  30133  clwwlkel  30135  clwwlkf  30136  clwwlkwwlksb  30143  1ewlk  30204  upgr3v3e3cycl  30269  upgr4cycl4dv4e  30274  dfconngr1  30277  isconngr1  30279  frgr3v  30364  frgrwopregasn  30405  frgrwopregbsn  30406  ubth  30963  acunirnmpt2  32752  acunirnmpt2f  32753  aciunf1  32755  fnpreimac  32762  fxpgaval  33247  crngmxidl  33548  lmxrge0  34116  measval  34362  isrnmeas  34364  sitgval  34496  eulerpartlemo  34529  eulerpartlemn  34545  onvf1odlem4  35308  subfacp1lem3  35384  subfacp1lem5  35386  txpconn  35434  cvxpconn  35444  cvmscbv  35460  cvmsi  35467  cvmsval  35468  satf  35555  sat1el2xp  35581  elmrsubrn  35722  weiunlem  36665  bj-raldifsn  37432  poimirlem26  37985  poimirlem27  37986  poimirlem31  37990  poimirlem32  37991  heicant  37994  mblfinlem3  37998  ovoliunnfl  38001  voliunnfl  38003  volsupnfl  38004  sdclem1  38082  fdc  38084  rrncmslem  38171  isass  38185  isrngod  38237  isgrpda  38294  iscom2  38334  pautsetN  40562  tendofset  41222  tendoset  41223  hdmap14lem13  42344  3factsumint1  42478  sticksstones3  42605  kelac1  43513  gicabl  43549  cantnfresb  43774  safesnsupfilb  43867  fiinfi  44022  clsk1independent  44495  scotteqd  44686  wessf1ornlem  45637  uzub  45881  rexanuz2nf  45942  mccl  46050  climsuse  46060  limsupmnfuzlem  46176  limsupmnfuz  46177  limsupre3uzlem  46185  limsupre3uz  46186  limsupreuz  46187  0cnv  46192  climuz  46194  lmbr3  46197  limsupgt  46228  liminflt  46255  xlimpnfxnegmnf  46264  xlimmnf  46291  xlimpnf  46292  xlimmnfmpt  46293  xlimpnfmpt  46294  dfxlim2  46298  fourierdlem2  46559  fourierdlem3  46560  fourierdlem31  46588  fourierdlem47  46603  fourierdlem70  46626  fourierdlem71  46627  fourierdlem80  46636  fourierdlem103  46659  fourierdlem104  46660  fourierdlem113  46669  etransclem48  46732  etransc  46733  caragenval  46943  omessle  46948  smfmullem2  47242  smfmul  47245  2ffzoeq  47792  iccpval  47891  iccpartigtl  47899  nprmmul1  48003  cycl3grtrilem  48438  grlimedgclnbgr  48487  grlimgrtri  48495  grilcbri2  48503  usgrexmpl2trifr  48529  gpg5nbgrvtx03star  48572  gpg5nbgr3star  48573  lindsrng01  48960  rrx2line  49232  initopropd  49734  termopropd  49735  fucofulem2  49802  thincpropd  49933  isinito2lem  49989