Theorem raleqdv 3121

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901

This theorem is referenced by:  raleqbidv  3129  raleqbidva  3131  raleleqALT  3134  raldifeq  4011  wfisg  5632  fveqressseq  6263  f12dfv  6429  f13dfv  6430  cbvfo  6444  isoselem  6491  ofrfval  6803  omsinds  6976  wfrlem4  7305  issmo2  7333  smoeq  7334  frfi  8090  marypha1lem  8222  marypha1  8223  dfoi  8299  oieq2  8301  ordtypecbv  8305  ordtypelem2  8307  ordtypelem3  8308  ordtypelem9  8314  wemapwe  8477  tcrank  8630  isacn  8750  pwsdompw  8909  isfin2  8999  isfin3ds  9034  isf33lem  9071  hsmexlem4  9134  zorn2lem6  9206  zorn2lem7  9207  zorn2g  9208  fpwwe2lem13  9343  uzsupss  11656  fzrevral2  12295  fzrevral3  12296  fzshftral  12297  fzoshftral  12447  uzsinds  12648  expmulnbnd  12858  eqs1  13245  swrdeq  13296  swrdspsleq  13301  2swrdeqwrdeq  13305  repswsymballbi  13378  cshw1  13419  wwlktovf1  13548  eqwrds3  13552  rexuz3  13936  rexuzre  13940  limsupgle  14056  rlim  14074  climconst  14122  rlimclim1  14124  climshftlem  14153  isercoll  14246  caucvgb  14258  serf0  14259  mertenslem1  14455  coprmprod  15213  coprmproddvds  15215  prmind2  15236  vdwlem10  15532  vdwlem13  15535  vdwnnlem2  15538  vdwnnlem3  15539  vdwnn  15540  ramval  15550  ramz  15567  prmgaplem5  15597  isacs  16135  cidpropd  16193  monpropd  16220  isssc  16303  fullsubc  16333  funcpropd  16383  isfth  16397  fthpropd  16404  grpidpropd  17084  mndpropd  17139  nmznsg  17461  ghmnsgima  17507  symgextfo  17665  gsmsymgrfixlem1  17670  gsmsymgrfix  17671  fvcosymgeq  17672  gsmsymgreqlem2  17674  symgfixf1  17680  psgnunilem3  17739  subgpgp  17835  sylow2blem3  17860  sylow3lem6  17870  efgsp1  17973  efgsres  17974  cmnpropd  18025  telgsumfzs  18209  ablfac2  18311  ringpropd  18405  abvpropd  18665  lsspropd  18838  lmhmpropd  18894  lbspropd  18920  pj1lmhm  18921  assapropd  19148  znf1o  19719  psgndiflemB  19765  phlpropd  19819  islindf  19970  lindfmm  19985  islindf4  19996  islindf5  19997  scmatf1  20156  isclo  20701  perfopn  20799  lmfval  20846  lmconst  20875  cncnp  20894  iscnrm2  20952  ist0-2  20958  ist1-2  20961  ishaus2  20965  ordtt1  20993  subislly  21094  elpt  21185  elptr  21186  ptbasfi  21194  tx1stc  21263  xkococnlem  21272  fclscmp  21644  ufilcmp  21646  cnpfcf  21655  alexsubALTlem1  21661  alexsubALTlem2  21662  alexsubALTlem4  21664  tmdgsum2  21710  tsmsf1o  21758  ustval  21816  ucnval  21891  imasdsf1olem  21988  imasf1oxmet  21990  imasf1omet  21991  metss  22123  prdsxmslem2  22144  cnmpt2pc  22535  lebnumlem3  22570  ishtpy  22579  pi1coghm  22669  lmnn  22869  evthicc  23035  cniccbdd  23037  ovolicc2lem4  23095  0pledm  23246  cniccibl  23413  c1lip1  23564  dvivthlem1  23575  lhop1  23581  itgsubstlem  23615  dgrlem  23789  ulmshftlem  23947  ulm0  23949  ulmcau  23953  iblulm  23965  rlimcnp  24492  xrlimcnp  24495  fsumdvdsmul  24721  chtub  24737  2sqlem10  24953  dchrisum0flb  24999  pntpbnd1  25075  pntpbnd  25077  pntibndlem2  25080  pntibndlem3  25081  pntibnd  25082  pntlemi  25093  pntleme  25097  pntlem3  25098  pntlemp  25099  pntleml  25100  pnt3  25101  istrkgld  25158  trgcgrg  25210  tgcgr4  25226  isperp  25407  brbtwn  25579  cusgra2v  25991  cusgra3v  25993  uvtxnb  26025  is2wlk  26095  constr1trl  26118  constr2wlk  26128  constr2trl  26129  redwlk  26136  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  usgrcyclnl2  26169  3v3e3cycl1  26172  constr3trllem2  26179  constr3trllem5  26182  4cycl4v4e  26194  4cycl4dv4e  26196  dfconngra1  26199  wwlknimp  26215  wlkiswwlk1  26218  wlkiswwlk2lem4  26222  wwlkn0s  26233  vfwlkniswwlkn  26234  2wlkeq  26235  usg2wlkeq  26236  wwlknred  26251  wwlknext  26252  clwwlkn2  26303  clwwlknimp  26304  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a  26313  clwlkisclwwlklem0  26316  clwwlkel  26321  clwwlkf  26322  wwlkext2clwwlk  26331  wwlksubclwwlk  26332  clwlkfclwwlk  26371  clwlkf1clwwlklem  26376  rusgranumwlkl1  26474  rusgra0edg  26482  eupai  26494  eupatrl  26495  eupa0  26501  eupares  26502  eupap1  26503  frgra3v  26529  frgrawopreg1  26577  extwwlkfablem2  26605  numclwwlkovf2ex  26613  ubth  27113  acunirnmpt2  28842  acunirnmpt2f  28843  aciunf1  28845  lmxrge0  29326  sigaclcu3  29512  measval  29588  isrnmeas  29590  sitgval  29721  eulerpartlemsv3  29750  eulerpartlemo  29754  eulerpartlemn  29770  bnj1514  30385  subfacp1lem3  30418  subfacp1lem5  30420  txpcon  30468  cvxpcon  30478  cvmscbv  30494  cvmsi  30501  cvmsval  30502  elmrsubrn  30671  frinsg  30986  poimirlem1  32580  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  poimirlem32  32611  heicant  32614  mblfinlem3  32618  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  cnicciblnc  32651  sdclem1  32709  fdc  32711  rrncmslem  32801  isass  32815  exidreslem  32846  exidresid  32848  isrngod  32867  isgrpda  32924  iscom2  32964  pautsetN  34402  tendofset  35064  tendoset  35065  hdmap14lem13  36190  kelac1  36651  gicabl  36687  lpirlnr  36706  fiinfi  36897  clsk1independent  37364  wessf1ornlem  38366  mccl  38665  climsuse  38675  fourierdlem2  39002  fourierdlem3  39003  fourierdlem31  39031  fourierdlem47  39046  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem80  39079  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  etransclem48  39175  etransc  39176  issal  39210  ismea  39344  caragenval  39383  isome  39384  omessle  39388  smfmullem2  39677  smfmul  39680  iccpval  39953  iccpartigtl  39961  pfxeq  40267  pfxsuffeqwrdeq  40269  pfx2  40275  2ffzoeq  40361  usgruspgrb  40411  usgr1e  40471  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  nbgr0vtx  40578  nbgr1vtx  40580  uvtxa01vtx0  40623  cplgr1v  40652  cusgrexi  40662  1hevtxdg0  40720  1wlkeq  40838  1wlkl1loop  40842  uspgr2wlkeq  40854  upgr2wlk  40876  red1wlk  40881  1wlkp1lem8  40889  usgr2wlkneq  40962  usgr2trlncl  40966  usgr2pthlem  40969  usgr2pth  40970  pthdlem1  40972  uspgrn2crct  41011  crctcsh1wlkn0lem7  41019  crctcsh1wlkn0  41024  wwlknp  41045  wwlksn0s  41057  1wlkiswwlks1  41064  1wlkiswwlks2lem4  41069  1wlkiswwlksupgr2  41074  wlknewwlksn  41084  wwlksnred  41098  wwlksnext  41099  rusgrnumwwlkl1  41172  clwwlknp  41195  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a  41207  clwlkclwwlklem3  41210  clwwlksn2  41217  clwwlksel  41221  clwwlksf  41222  wwlksext2clwwlk  41231  wwlksubclwwlks  41232  clwlksfclwwlk  41269  clwlksf1clwwlklem  41275  1ewlk  41283  11wlkdlem4  41307  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  dfconngr1  41355  isconngr1  41357  frgr1v  41441  frgr3v  41445  frgrwopreg1  41487  av-numclwwlkovf2ex  41517  c0snmgmhm  41704  linds0  42048  lindsrng01  42051