Theorem raleqdv 3319

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ral 3077  df-rex 3087

This theorem is used by:  raleqtrdv  3321  raleqtrrdv  3323  raleqbidva  3325  raldifeq  4449  frpoinsg  6341  f12dfv  7274  f13dfv  7275  cbvfo  7290  isoselem  7342  ofrfvalg  7686  omsinds  7883  frpoins3xpg  8138  frpoins3xp3g  8139  frrlem4  8288  issmo2  8338  smoeq  8339  on2ind  8657  on3ind  8658  naddsuc2  8690  frfi  9255  marypha1lem  9403  marypha1  9404  dfoi  9483  oieq2  9485  ordtypecbv  9489  ordtypelem2  9491  ordtypelem3  9492  ordtypelem9  9498  wemapwe  9676  ttrclss  9699  ttrclselem2  9705  frinsg  9733  tcrank  9866  scotteqd  9869  isacn  10047  pwsdompw  10205  isfin2  10296  isfin3ds  10331  isf33lem  10368  hsmexlem4  10431  zorn2lem6  10503  zorn2lem7  10504  zorn2g  10505  fpwwe2lem12  10651  uzsupss  12989  fzrevral2  13668  fzrevral3  13669  fzshftral  13670  fzoshftral  13843  uzsinds  14051  expmulnbnd  14299  eqs1  14680  swrdspsleq  14735  pfxeq  14765  pfxsuffeqwrdeq  14767  repswsymballbi  14851  cshw1  14893  pfx2  15018  wwlktovf1  15030  eqwrds3  15034  rexuz3  15436  rexuzre  15440  limsupgle  15564  rlim  15582  climconst  15630  rlimclim1  15632  climshftlem  15661  isercoll  15755  caucvgb  15767  serf0  15768  mertenslem1  15973  coprmprod  16751  coprmproddvds  16753  prmind2  16775  vdwlem10  17082  vdwlem13  17085  vdwnnlem2  17088  vdwnnlem3  17089  vdwnn  17090  ramval  17100  ramz  17117  prmgaplem5  17147  isacs  17739  cidpropd  17798  monpropd  17826  isssc  17909  fullsubc  17939  funcpropd  17991  isfth  18005  fthpropd  18012  grpidpropd  18755  sgrppropd  18833  mndpropd  18864  nmznsg  19291  ghmnsgima  19367  symgextfo  19549  gsmsymgrfixlem1  19554  gsmsymgrfix  19555  fvcosymgeq  19556  gsmsymgreqlem2  19558  psgnunilem3  19623  sylow2blem3  19749  sylow3lem6  19759  cmnpropd  19918  telgsumfzs  20116  rngpropd  20309  ringpropd  20430  c0snmgmhm  20603  abvpropd  21001  lsspropd  21201  lmhmpropd  21257  lbspropd  21283  pj1lmhm  21284  psgndiflemB  21813  phlpropd  21868  islindf  22025  lindfmm  22040  islindf4  22051  islindf5  22052  assapropd  22086  scmatf1  22753  isclo  23312  lmfval  23457  lmconst  23486  iscnrm2  23563  ist0-2  23569  ist1-2  23572  ishaus2  23576  subislly  23707  elpt  23798  elptr  23799  ptbasfi  23807  fclscmp  24256  ufilcmp  24258  cnpfcf  24267  alexsubALTlem1  24273  alexsubALTlem2  24274  alexsubALTlem4  24276  tmdgsum2  24322  tsmsf1o  24371  ustval  24429  ucnval  24502  imasdsf1olem  24599  imasf1oxmet  24601  imasf1omet  24602  metss  24734  prdsxmslem2  24755  lebnumlem3  25191  ishtpy  25200  lmnn  25491  evthicc  25687  cniccbdd  25689  ovolicc2lem4  25748  0pledm  25901  cniccibl  26068  cnicciblnc  26070  c1lip1  26224  lhop1  26241  itgsubstlem  26275  ulmshftlem  26625  ulm0  26627  ulmcau  26631  rlimcnp  27202  fsumdvdsmul  27431  chtub  27448  2sqlem10  27664  dchrisum0flb  27746  pntpbnd1  27822  pntpbnd  27824  pntibndlem2  27827  pntibndlem3  27828  pntibnd  27829  pntlemi  27840  pntleme  27844  pntlem3  27845  pntlemp  27846  pntleml  27847  pnt3  27848  madebdaylemlrcut  28164  noinds  28210  no2indlesm  28219  no3inds  28223  precsexlem9  28480  istrkgld  28800  trgcgrg  28857  tgcgr4  28873  isperp  29066  brbtwn  29356  usgruspgrb  29643  nbgr2vtx1edg  29810  nbuhgr2vtx1edgb  29812  nbgr1vtx  29818  uvtx01vtx  29857  cplgr1v  29890  wlkeq  30093  wlkl1loop  30097  uspgr2wlkeq  30105  upgr2wlk  30126  redwlk  30130  wlkp1lem8  30138  usgr2wlkneq  30221  usgr2trlncl  30225  usgr2pthlem  30228  usgr2pth  30229  pthdlem1  30231  uspgrn2crct  30276  crctcshwlkn0  30289  wwlknp  30311  wwlksn0s  30329  wlkiswwlks1  30335  wlkiswwlks2lem4  30340  wwlksnred  30360  rusgrnumwwlkl1  30439  clwwlkccatlem  30459  clwlkclwwlklem2a1  30462  clwlkclwwlklem2a  30468  clwlkclwwlklem3  30471  clwwlkn  30496  clwwlknp  30507  clwwlkinwwlk  30510  clwwlkn1  30511  clwwlkn2  30514  clwwlkel  30516  clwwlkf  30517  clwwlkwwlksb  30524  1ewlk  30585  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  dfconngr1  30668  isconngr1  30670  frgr3v  30755  frgrwopregasn  30796  frgrwopregbsn  30797  ubth  31354  acunirnmpt2  33133  acunirnmpt2f  33134  aciunf1  33136  fnpreimac  33143  fxpgaval  33607  crngmxidl  33872  lmxrge0  34462  measval  34709  isrnmeas  34711  sitgval  34843  eulerpartlemo  34876  eulerpartlemn  34892  onvf1odlem4  35703  subfacp1lem3  35761  subfacp1lem5  35763  txpconn  35811  cvxpconn  35821  cvmscbv  35837  cvmsi  35844  cvmsval  35845  satf  35932  sat1el2xp  35958  elmrsubrn  36099  weiunlem  37082  bj-raldifsn  37850  poimirlem26  38395  poimirlem27  38396  poimirlem31  38400  poimirlem32  38401  heicant  38404  mblfinlem3  38408  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  sdclem1  38493  fdc  38495  rrncmslem  38582  isass  38596  isrngod  38648  isgrpda  38705  iscom2  38745  pautsetN  40971  tendofset  41631  tendoset  41632  hdmap14lem13  42753  3factsumint1  42887  sticksstones3  43014  kelac1  43904  gicabl  43940  cantnfresb  44165  safesnsupfilb  44258  fiinfi  44413  clsk1independent  44886  wessf1ornlem  46017  uzub  46259  rexanuz2nf  46320  mccl  46428  climsuse  46438  limsupmnfuzlem  46554  limsupmnfuz  46555  limsupre3uzlem  46563  limsupre3uz  46564  limsupreuz  46565  0cnv  46570  climuz  46572  lmbr3  46575  limsupgt  46606  liminflt  46633  xlimpnfxnegmnf  46642  xlimmnf  46669  xlimpnf  46670  xlimmnfmpt  46671  xlimpnfmpt  46672  dfxlim2  46676  fourierdlem2  46937  fourierdlem3  46938  fourierdlem31  46966  fourierdlem47  46981  fourierdlem70  47004  fourierdlem71  47005  fourierdlem80  47014  fourierdlem103  47037  fourierdlem104  47038  fourierdlem113  47047  etransclem48  47110  etransc  47111  caragenval  47321  omessle  47326  smfmullem2  47620  smfmul  47623  2ffzoeq  48216  iccpval  48315  iccpartigtl  48323  nprmmul1  48427  cycl3grtrilem  48862  grlimedgclnbgr  48911  grlimgrtri  48919  grilcbri2  48927  usgrexmpl2trifr  48953  gpg5nbgrvtx03star  48996  gpg5nbgr3star  48997  lindsrng01  49398  rrx2line  49670  initopropd  50169  termopropd  50170  fucofulem2  50237  thincpropd  50368  isinito2lem  50424