Theorem raleqdv 3299

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-ral 3056  df-rex 3066

This theorem is referenced by:  raleqtrdv  3301  raleqtrrdv  3303  raleqbidva  3305  raleleqOLD  3312  raldifeq  4424  frpoinsg  6298  f12dfv  7221  f13dfv  7222  cbvfo  7237  isoselem  7289  ofrfvalg  7632  omsinds  7831  frpoins3xpg  8084  frpoins3xp3g  8085  frrlem4  8233  issmo2  8283  smoeq  8284  on2ind  8599  on3ind  8600  naddsuc2  8631  frfi  9189  marypha1lem  9340  marypha1  9341  dfoi  9420  oieq2  9422  ordtypecbv  9426  ordtypelem2  9428  ordtypelem3  9429  ordtypelem9  9435  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  20811  lsspropd  21011  lmhmpropd  21067  lbspropd  21093  pj1lmhm  21094  psgndiflemB  21579  phlpropd  21634  islindf  21791  lindfmm  21806  islindf4  21817  islindf5  21818  assapropd  21850  scmatf1  22518  isclo  23074  lmfval  23219  lmconst  23248  iscnrm2  23325  ist0-2  23331  ist1-2  23334  ishaus2  23338  subislly  23468  elpt  23559  elptr  23560  ptbasfi  23568  fclscmp  24017  ufilcmp  24019  cnpfcf  24028  alexsubALTlem1  24034  alexsubALTlem2  24035  alexsubALTlem4  24037  tmdgsum2  24083  tsmsf1o  24132  ustval  24190  ucnval  24263  imasdsf1olem  24360  imasf1oxmet  24362  imasf1omet  24363  metss  24495  prdsxmslem2  24516  lebnumlem3  24952  ishtpy  24961  lmnn  25252  evthicc  25448  cniccbdd  25450  ovolicc2lem4  25509  0pledm  25662  cniccibl  25830  cnicciblnc  25832  c1lip1  25986  lhop1  26003  itgsubstlem  26037  ulmshftlem  26376  ulm0  26378  ulmcau  26382  rlimcnp  26951  fsumdvdsmul  27180  chtub  27197  2sqlem10  27413  dchrisum0flb  27495  pntpbnd1  27571  pntpbnd  27573  pntibndlem2  27576  pntibndlem3  27577  pntibnd  27578  pntlemi  27589  pntleme  27593  pntlem3  27594  pntlemp  27595  pntleml  27596  pnt3  27597  madebdaylemlrcut  27913  noinds  27959  no2indlesm  27968  no3inds  27972  precsexlem9  28229  istrkgld  28549  trgcgrg  28605  tgcgr4  28621  isperp  28802  brbtwn  28990  usgruspgrb  29274  nbgr2vtx1edg  29441  nbuhgr2vtx1edgb  29443  nbgr1vtx  29449  uvtx01vtx  29488  cplgr1v  29521  wlkeq  29724  wlkl1loop  29728  uspgr2wlkeq  29736  upgr2wlk  29757  redwlk  29761  wlkp1lem8  29769  usgr2wlkneq  29846  usgr2trlncl  29850  usgr2pthlem  29853  usgr2pth  29854  pthdlem1  29856  uspgrn2crct  29898  crctcshwlkn0  29911  wwlknp  29933  wwlksn0s  29951  wlkiswwlks1  29957  wlkiswwlks2lem4  29962  wwlksnred  29982  rusgrnumwwlkl1  30061  clwwlkccatlem  30081  clwlkclwwlklem2a1  30084  clwlkclwwlklem2a  30090  clwlkclwwlklem3  30093  clwwlkn  30118  clwwlknp  30129  clwwlkinwwlk  30132  clwwlkn1  30133  clwwlkn2  30136  clwwlkel  30138  clwwlkf  30139  clwwlkwwlksb  30146  1ewlk  30207  upgr3v3e3cycl  30272  upgr4cycl4dv4e  30277  dfconngr1  30280  isconngr1  30282  frgr3v  30367  frgrwopregasn  30408  frgrwopregbsn  30409  ubth  30966  acunirnmpt2  32756  acunirnmpt2f  32757  aciunf1  32759  fnpreimac  32766  fxpgaval  33252  crngmxidl  33556  lmxrge0  34148  measval  34394  isrnmeas  34396  sitgval  34528  eulerpartlemo  34561  eulerpartlemn  34577  onvf1odlem4  35349  subfacp1lem3  35425  subfacp1lem5  35427  txpconn  35475  cvxpconn  35485  cvmscbv  35501  cvmsi  35508  cvmsval  35509  satf  35596  sat1el2xp  35622  elmrsubrn  35763  weiunlem  36706  bj-raldifsn  37473  poimirlem26  38028  poimirlem27  38029  poimirlem31  38033  poimirlem32  38034  heicant  38037  mblfinlem3  38041  ovoliunnfl  38044  voliunnfl  38046  volsupnfl  38047  sdclem1  38125  fdc  38127  rrncmslem  38214  isass  38228  isrngod  38280  isgrpda  38337  iscom2  38377  pautsetN  40605  tendofset  41265  tendoset  41266  hdmap14lem13  42387  3factsumint1  42521  sticksstones3  42648  kelac1  43523  gicabl  43559  cantnfresb  43784  safesnsupfilb  43877  fiinfi  44032  clsk1independent  44505  scotteqd  44696  wessf1ornlem  45646  uzub  45888  rexanuz2nf  45949  mccl  46057  climsuse  46067  limsupmnfuzlem  46183  limsupmnfuz  46184  limsupre3uzlem  46192  limsupre3uz  46193  limsupreuz  46194  0cnv  46199  climuz  46201  lmbr3  46204  limsupgt  46235  liminflt  46262  xlimpnfxnegmnf  46271  xlimmnf  46298  xlimpnf  46299  xlimmnfmpt  46300  xlimpnfmpt  46301  dfxlim2  46305  fourierdlem2  46566  fourierdlem3  46567  fourierdlem31  46595  fourierdlem47  46610  fourierdlem70  46633  fourierdlem71  46634  fourierdlem80  46643  fourierdlem103  46666  fourierdlem104  46667  fourierdlem113  46676  etransclem48  46739  etransc  46740  caragenval  46950  omessle  46955  smfmullem2  47249  smfmul  47252  2ffzoeq  47805  iccpval  47904  iccpartigtl  47912  nprmmul1  48016  cycl3grtrilem  48451  grlimedgclnbgr  48500  grlimgrtri  48508  grilcbri2  48516  usgrexmpl2trifr  48542  gpg5nbgrvtx03star  48585  gpg5nbgr3star  48586  lindsrng01  48973  rrx2line  49245  initopropd  49747  termopropd  49748  fucofulem2  49815  thincpropd  49946  isinito2lem  50002