Theorem raleqdv 3322

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-ral 3079  df-rex 3089

This theorem is referenced by:  raleqtrdv  3324  raleqtrrdv  3326  raleqbidva  3328  raleleqOLD  3335  raldifeq  4449  frpoinsg  6332  f12dfv  7259  f13dfv  7260  cbvfo  7275  isoselem  7327  ofrfvalg  7670  omsinds  7869  frpoins3xpg  8122  frpoins3xp3g  8123  frrlem4  8272  issmo2  8322  smoeq  8323  on2ind  8641  on3ind  8642  naddsuc2  8674  frfi  9231  marypha1lem  9381  marypha1  9382  dfoi  9461  oieq2  9463  ordtypecbv  9467  ordtypelem2  9469  ordtypelem3  9470  ordtypelem9  9476  wemapwe  9654  ttrclss  9677  ttrclselem2  9683  frinsg  9711  tcrank  9844  isacn  10002  pwsdompw  10161  isfin2  10253  isfin3ds  10288  isf33lem  10325  hsmexlem4  10388  zorn2lem6  10460  zorn2lem7  10461  zorn2g  10462  fpwwe2lem12  10602  uzsupss  12943  fzrevral2  13620  fzrevral3  13621  fzshftral  13622  fzoshftral  13795  uzsinds  14002  expmulnbnd  14250  eqs1  14628  swrdspsleq  14681  pfxeq  14711  pfxsuffeqwrdeq  14713  repswsymballbi  14795  cshw1  14837  pfx2  14962  wwlktovf1  14972  eqwrds3  14976  rexuz3  15378  rexuzre  15382  limsupgle  15506  rlim  15524  climconst  15572  rlimclim1  15574  climshftlem  15603  isercoll  15697  caucvgb  15709  serf0  15710  mertenslem1  15916  coprmprod  16697  coprmproddvds  16699  prmind2  16721  vdwlem10  17028  vdwlem13  17031  vdwnnlem2  17034  vdwnnlem3  17035  vdwnn  17036  ramval  17046  ramz  17063  prmgaplem5  17093  isacs  17685  cidpropd  17744  monpropd  17772  isssc  17855  fullsubc  17885  funcpropd  17937  isfth  17951  fthpropd  17958  grpidpropd  18698  sgrppropd  18767  mndpropd  18795  nmznsg  19211  ghmnsgima  19282  symgextfo  19464  gsmsymgrfixlem1  19469  gsmsymgrfix  19470  fvcosymgeq  19471  gsmsymgreqlem2  19473  psgnunilem3  19538  sylow2blem3  19664  sylow3lem6  19674  cmnpropd  19833  telgsumfzs  20031  rngpropd  20222  ringpropd  20340  c0snmgmhm  20513  abvpropd  20886  lsspropd  21086  lmhmpropd  21142  lbspropd  21168  pj1lmhm  21169  psgndiflemB  21654  phlpropd  21709  islindf  21866  lindfmm  21881  islindf4  21892  islindf5  21893  assapropd  21925  scmatf1  22593  isclo  23149  lmfval  23294  lmconst  23323  iscnrm2  23400  ist0-2  23406  ist1-2  23409  ishaus2  23413  subislly  23543  elpt  23634  elptr  23635  ptbasfi  23643  fclscmp  24092  ufilcmp  24094  cnpfcf  24103  alexsubALTlem1  24109  alexsubALTlem2  24110  alexsubALTlem4  24112  tmdgsum2  24158  tsmsf1o  24207  ustval  24265  ucnval  24338  imasdsf1olem  24435  imasf1oxmet  24437  imasf1omet  24438  metss  24570  prdsxmslem2  24591  lebnumlem3  25027  ishtpy  25036  lmnn  25327  evthicc  25523  cniccbdd  25525  ovolicc2lem4  25584  0pledm  25737  cniccibl  25905  cnicciblnc  25907  c1lip1  26061  lhop1  26078  itgsubstlem  26112  ulmshftlem  26454  ulm0  26456  ulmcau  26460  rlimcnp  27032  fsumdvdsmul  27261  chtub  27278  2sqlem10  27494  dchrisum0flb  27576  pntpbnd1  27652  pntpbnd  27654  pntibndlem2  27657  pntibndlem3  27658  pntibnd  27659  pntlemi  27670  pntleme  27674  pntlem3  27675  pntlemp  27676  pntleml  27677  pnt3  27678  madebdaylemlrcut  27994  noinds  28040  no2indlesm  28049  no3inds  28053  precsexlem9  28310  istrkgld  28630  trgcgrg  28686  tgcgr4  28702  isperp  28887  brbtwn  29102  usgruspgrb  29386  nbgr2vtx1edg  29553  nbuhgr2vtx1edgb  29555  nbgr1vtx  29561  uvtx01vtx  29600  cplgr1v  29633  wlkeq  29836  wlkl1loop  29840  uspgr2wlkeq  29848  upgr2wlk  29869  redwlk  29873  wlkp1lem8  29881  usgr2wlkneq  29958  usgr2trlncl  29962  usgr2pthlem  29965  usgr2pth  29966  pthdlem1  29968  uspgrn2crct  30010  crctcshwlkn0  30023  wwlknp  30045  wwlksn0s  30063  wlkiswwlks1  30069  wlkiswwlks2lem4  30074  wwlksnred  30094  rusgrnumwwlkl1  30173  clwwlkccatlem  30193  clwlkclwwlklem2a1  30196  clwlkclwwlklem2a  30202  clwlkclwwlklem3  30205  clwwlkn  30230  clwwlknp  30241  clwwlkinwwlk  30244  clwwlkn1  30245  clwwlkn2  30248  clwwlkel  30250  clwwlkf  30251  clwwlkwwlksb  30258  1ewlk  30319  upgr3v3e3cycl  30384  upgr4cycl4dv4e  30389  dfconngr1  30392  isconngr1  30394  frgr3v  30479  frgrwopregasn  30520  frgrwopregbsn  30521  ubth  31078  acunirnmpt2  32864  acunirnmpt2f  32865  aciunf1  32867  fnpreimac  32874  fxpgaval  33349  crngmxidl  33659  lmxrge0  34251  measval  34497  isrnmeas  34499  sitgval  34631  eulerpartlemo  34664  eulerpartlemn  34680  onvf1odlem4  35453  subfacp1lem3  35537  subfacp1lem5  35539  txpconn  35587  cvxpconn  35597  cvmscbv  35613  cvmsi  35620  cvmsval  35621  satf  35708  sat1el2xp  35734  elmrsubrn  35875  weiunlem  36828  bj-raldifsn  37595  poimirlem26  38150  poimirlem27  38151  poimirlem31  38155  poimirlem32  38156  heicant  38159  mblfinlem3  38163  ovoliunnfl  38166  voliunnfl  38168  volsupnfl  38169  sdclem1  38247  fdc  38249  rrncmslem  38336  isass  38350  isrngod  38402  isgrpda  38459  iscom2  38499  pautsetN  40727  tendofset  41387  tendoset  41388  hdmap14lem13  42509  3factsumint1  42643  sticksstones3  42770  kelac1  43645  gicabl  43681  cantnfresb  43906  safesnsupfilb  43999  fiinfi  44154  clsk1independent  44627  scotteqd  44818  wessf1ornlem  45768  uzub  46010  rexanuz2nf  46071  mccl  46179  climsuse  46189  limsupmnfuzlem  46305  limsupmnfuz  46306  limsupre3uzlem  46314  limsupre3uz  46315  limsupreuz  46316  0cnv  46321  climuz  46323  lmbr3  46326  limsupgt  46357  liminflt  46384  xlimpnfxnegmnf  46393  xlimmnf  46420  xlimpnf  46421  xlimmnfmpt  46422  xlimpnfmpt  46423  dfxlim2  46427  fourierdlem2  46688  fourierdlem3  46689  fourierdlem31  46717  fourierdlem47  46732  fourierdlem70  46755  fourierdlem71  46756  fourierdlem80  46765  fourierdlem103  46788  fourierdlem104  46789  fourierdlem113  46798  etransclem48  46861  etransc  46862  caragenval  47072  omessle  47077  smfmullem2  47371  smfmul  47374  2ffzoeq  47927  iccpval  48026  iccpartigtl  48034  nprmmul1  48138  cycl3grtrilem  48573  grlimedgclnbgr  48622  grlimgrtri  48630  grilcbri2  48638  usgrexmpl2trifr  48664  gpg5nbgrvtx03star  48707  gpg5nbgr3star  48708  lindsrng01  49095  rrx2line  49367  initopropd  49869  termopropd  49870  fucofulem2  49937  thincpropd  50068  isinito2lem  50124