Theorem raleqdv 3339

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ral 3068

This theorem is referenced by:  raleqbidva  3345  raleleqALT  3348  raldifeq  4421  frpoinsg  6231  wfisgOLD  6242  fveqressseq  6939  f12dfv  7126  f13dfv  7127  cbvfo  7141  isoselem  7192  ofrfvalg  7519  omsinds  7708  omsindsOLD  7709  frrlem4  8076  wfrlem4OLD  8114  issmo2  8151  smoeq  8152  frfi  8989  marypha1lem  9122  marypha1  9123  dfoi  9200  oieq2  9202  ordtypecbv  9206  ordtypelem2  9208  ordtypelem3  9209  ordtypelem9  9215  wemapwe  9385  frinsg  9440  tcrank  9573  isacn  9731  pwsdompw  9891  isfin2  9981  isfin3ds  10016  isf33lem  10053  hsmexlem4  10116  zorn2lem6  10188  zorn2lem7  10189  zorn2g  10190  fpwwe2lem12  10329  uzsupss  12609  fzrevral2  13271  fzrevral3  13272  fzshftral  13273  fzoshftral  13432  uzsinds  13635  expmulnbnd  13878  eqs1  14245  swrdspsleq  14306  pfxeq  14337  pfxsuffeqwrdeq  14339  repswsymballbi  14421  cshw1  14463  pfx2  14588  wwlktovf1  14600  eqwrds3  14604  rexuz3  14988  rexuzre  14992  limsupgle  15114  rlim  15132  climconst  15180  rlimclim1  15182  climshftlem  15211  isercoll  15307  caucvgb  15319  serf0  15320  mertenslem1  15524  coprmprod  16294  coprmproddvds  16296  prmind2  16318  vdwlem10  16619  vdwlem13  16622  vdwnnlem2  16625  vdwnnlem3  16626  vdwnn  16627  ramval  16637  ramz  16654  prmgaplem5  16684  isacs  17277  cidpropd  17336  monpropd  17366  isssc  17449  fullsubc  17481  funcpropd  17532  isfth  17546  fthpropd  17553  grpidpropd  18261  mndpropd  18325  nmznsg  18711  ghmnsgima  18773  symgextfo  18945  gsmsymgrfixlem1  18950  gsmsymgrfix  18951  fvcosymgeq  18952  gsmsymgreqlem2  18954  symgfixf1  18960  psgnunilem3  19019  subgpgp  19117  sylow2blem3  19142  sylow3lem6  19152  efgsp1  19258  efgsres  19259  cmnpropd  19311  telgsumfzs  19505  ablfac2  19607  ringpropd  19736  abvpropd  20017  lsspropd  20194  lmhmpropd  20250  lbspropd  20276  pj1lmhm  20277  znf1o  20671  psgndiflemB  20717  phlpropd  20772  islindf  20929  lindfmm  20944  islindf4  20955  islindf5  20956  assapropd  20986  scmatf1  21588  isclo  22146  perfopn  22244  lmfval  22291  lmconst  22320  cncnp  22339  iscnrm2  22397  ist0-2  22403  ist1-2  22406  ishaus2  22410  ordtt1  22438  subislly  22540  elpt  22631  elptr  22632  ptbasfi  22640  tx1stc  22709  xkococnlem  22718  fclscmp  23089  ufilcmp  23091  cnpfcf  23100  alexsubALTlem1  23106  alexsubALTlem2  23107  alexsubALTlem4  23109  tmdgsum2  23155  tsmsf1o  23204  ustval  23262  ucnval  23337  imasdsf1olem  23434  imasf1oxmet  23436  imasf1omet  23437  metss  23570  prdsxmslem2  23591  cnmpopc  23997  lebnumlem3  24032  ishtpy  24041  pi1coghm  24130  lmnn  24332  evthicc  24528  cniccbdd  24530  ovolicc2lem4  24589  0pledm  24742  cniccibl  24910  cnicciblnc  24912  c1lip1  25066  dvivthlem1  25077  lhop1  25083  itgsubstlem  25117  dgrlem  25295  ulmshftlem  25453  ulm0  25455  ulmcau  25459  iblulm  25471  rlimcnp  26020  xrlimcnp  26023  fsumdvdsmul  26249  chtub  26265  2sqlem10  26481  dchrisum0flb  26563  pntpbnd1  26639  pntpbnd  26641  pntibndlem2  26644  pntibndlem3  26645  pntibnd  26646  pntlemi  26657  pntleme  26661  pntlem3  26662  pntlemp  26663  pntleml  26664  pnt3  26665  istrkgld  26724  trgcgrg  26780  tgcgr4  26796  isperp  26977  brbtwn  27170  usgruspgrb  27454  usgr1e  27515  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  nbgr0vtx  27626  nbgr1vtx  27628  uvtx01vtx  27667  cplgr1v  27700  cusgrexi  27713  1hevtxdg0  27775  wlkeq  27903  wlkl1loop  27907  uspgr2wlkeq  27915  upgr2wlk  27938  redwlk  27942  wlkp1lem8  27950  usgr2wlkneq  28025  usgr2trlncl  28029  usgr2pthlem  28032  usgr2pth  28033  pthdlem1  28035  uspgrn2crct  28074  crctcshwlkn0lem7  28082  crctcshwlkn0  28087  wwlknp  28109  wwlksn0s  28127  wlkiswwlks1  28133  wlkiswwlks2lem4  28138  wlkiswwlksupgr2  28143  wlknewwlksn  28153  wwlksnred  28158  wwlksnext  28159  rusgrnumwwlkl1  28234  clwwlkccatlem  28254  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a  28263  clwlkclwwlklem3  28266  clwlkclwwlkf1lem3  28271  clwwlkn  28291  clwwlknp  28302  clwwlkinwwlk  28305  clwwlkn1  28306  clwwlkn2  28309  clwwlkel  28311  clwwlkf  28312  clwwlkwwlksb  28319  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  clwwlknonex2  28374  1ewlk  28380  1wlkdlem4  28405  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  dfconngr1  28453  isconngr1  28455  frgr3v  28540  frgrwopregasn  28581  frgrwopregbsn  28582  ubth  29136  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1  30902  fnpreimac  30910  lmxrge0  31804  sigaclcu3  31990  measval  32066  isrnmeas  32068  sitgval  32199  eulerpartlemsv3  32228  eulerpartlemo  32232  eulerpartlemn  32248  bnj1514  32943  subfacp1lem3  33044  subfacp1lem5  33046  txpconn  33094  cvxpconn  33104  cvmscbv  33120  cvmsi  33127  cvmsval  33128  satf  33215  sat1el2xp  33241  elmrsubrn  33382  ttrclss  33706  ttrclselem2  33712  frpoins3xpg  33714  frpoins3xp3g  33715  on2ind  33755  on3ind  33756  madebdaylemlrcut  34006  noinds  34029  no2indslem  34038  no3inds  34042  bj-raldifsn  35198  poimirlem1  35705  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  poimirlem32  35736  heicant  35739  mblfinlem3  35743  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  sdclem1  35828  fdc  35830  rrncmslem  35917  isass  35931  exidreslem  35962  exidresid  35964  isrngod  35983  isgrpda  36040  iscom2  36080  pautsetN  38039  tendofset  38699  tendoset  38700  hdmap14lem13  39821  3factsumint1  39957  sticksstones3  40032  kelac1  40804  gicabl  40840  lpirlnr  40858  fiinfi  41069  clsk1independent  41545  scotteqd  41744  wessf1ornlem  42611  uzub  42861  mccl  43029  climsuse  43039  limsupmnfuzlem  43157  limsupmnfuz  43158  limsupre3uzlem  43166  limsupre3uz  43167  limsupreuz  43168  0cnv  43173  climuz  43175  lmbr3  43178  limsupgt  43209  liminflt  43236  xlimpnfxnegmnf  43245  xlimmnf  43272  xlimpnf  43273  xlimmnfmpt  43274  xlimpnfmpt  43275  dfxlim2  43279  fourierdlem2  43540  fourierdlem3  43541  fourierdlem31  43569  fourierdlem47  43584  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem80  43617  fourierdlem103  43640  fourierdlem104  43641  fourierdlem113  43650  etransclem48  43713  etransc  43714  caragenval  43921  omessle  43926  smfmullem2  44213  smfmul  44216  2ffzoeq  44708  iccpval  44755  iccpartigtl  44763  c0snmgmhm  45360  linds0  45694  lindsrng01  45697  rrx2line  45974