Theorem raleqdv 3356

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1656  ∀wral 3117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122

This theorem is referenced by:  raleqbidv  3364  raleqbidva  3366  raleleqALT  3369  raldifeq  4283  wfisg  5959  fveqressseq  6609  f12dfv  6789  f13dfv  6790  cbvfo  6804  isoselem  6851  ofrfval  7170  omsinds  7350  wfrlem4  7688  wfrlem4OLD  7689  issmo2  7717  smoeq  7718  frfi  8480  marypha1lem  8614  marypha1  8615  dfoi  8692  oieq2  8694  ordtypecbv  8698  ordtypelem2  8700  ordtypelem3  8701  ordtypelem9  8707  wemapwe  8878  tcrank  9031  isacn  9187  pwsdompw  9348  isfin2  9438  isfin3ds  9473  isf33lem  9510  hsmexlem4  9573  zorn2lem6  9645  zorn2lem7  9646  zorn2g  9647  fpwwe2lem13  9786  uzsupss  12070  fzrevral2  12727  fzrevral3  12728  fzshftral  12729  fzoshftral  12887  uzsinds  13088  expmulnbnd  13297  eqs1  13679  swrdeqOLD  13740  swrdspsleq  13746  2swrdeqwrdeqOLD  13750  pfxeq  13782  pfxsuffeqwrdeq  13784  repswsymballbi  13903  cshw1  13950  pfx2  14075  wwlktovf1  14086  eqwrds3  14090  rexuz3  14472  rexuzre  14476  limsupgle  14592  rlim  14610  climconst  14658  rlimclim1  14660  climshftlem  14689  isercoll  14782  caucvgb  14794  serf0  14795  mertenslem1  14996  coprmprod  15754  coprmproddvds  15756  prmind2  15777  vdwlem10  16072  vdwlem13  16075  vdwnnlem2  16078  vdwnnlem3  16079  vdwnn  16080  ramval  16090  ramz  16107  prmgaplem5  16137  isacs  16671  cidpropd  16729  monpropd  16756  isssc  16839  fullsubc  16869  funcpropd  16919  isfth  16933  fthpropd  16940  grpidpropd  17621  mndpropd  17676  nmznsg  17996  ghmnsgima  18042  symgextfo  18199  gsmsymgrfixlem1  18204  gsmsymgrfix  18205  fvcosymgeq  18206  gsmsymgreqlem2  18208  symgfixf1  18214  psgnunilem3  18274  subgpgp  18370  sylow2blem3  18395  sylow3lem6  18405  efgsp1  18508  efgsres  18509  efgsresOLD  18510  cmnpropd  18562  telgsumfzs  18747  ablfac2  18849  ringpropd  18943  abvpropd  19205  lsspropd  19383  lmhmpropd  19439  lbspropd  19465  pj1lmhm  19466  assapropd  19695  znf1o  20266  psgndiflemB  20313  phlpropd  20369  islindf  20525  lindfmm  20540  islindf4  20551  islindf5  20552  scmatf1  20712  isclo  21269  perfopn  21367  lmfval  21414  lmconst  21443  cncnp  21462  iscnrm2  21520  ist0-2  21526  ist1-2  21529  ishaus2  21533  ordtt1  21561  subislly  21662  elpt  21753  elptr  21754  ptbasfi  21762  tx1stc  21831  xkococnlem  21840  fclscmp  22211  ufilcmp  22213  cnpfcf  22222  alexsubALTlem1  22228  alexsubALTlem2  22229  alexsubALTlem4  22231  tmdgsum2  22277  tsmsf1o  22325  ustval  22383  ucnval  22458  imasdsf1olem  22555  imasf1oxmet  22557  imasf1omet  22558  metss  22690  prdsxmslem2  22711  cnmpt2pc  23104  lebnumlem3  23139  ishtpy  23148  pi1coghm  23237  lmnn  23438  evthicc  23632  cniccbdd  23634  ovolicc2lem4  23693  0pledm  23846  cniccibl  24013  c1lip1  24166  dvivthlem1  24177  lhop1  24183  itgsubstlem  24217  dgrlem  24391  ulmshftlem  24549  ulm0  24551  ulmcau  24555  iblulm  24567  rlimcnp  25112  xrlimcnp  25115  fsumdvdsmul  25341  chtub  25357  2sqlem10  25573  dchrisum0flb  25619  pntpbnd1  25695  pntpbnd  25697  pntibndlem2  25700  pntibndlem3  25701  pntibnd  25702  pntlemi  25713  pntleme  25717  pntlem3  25718  pntlemp  25719  pntleml  25720  pnt3  25721  istrkgld  25778  trgcgrg  25834  tgcgr4  25850  isperp  26031  brbtwn  26205  usgruspgrb  26487  usgr1e  26549  nbgr2vtx1edg  26654  nbuhgr2vtx1edgb  26656  nbgr0vtx  26660  nbgr1vtx  26662  uvtx01vtx  26702  cplgr1v  26735  cusgrexi  26748  1hevtxdg0  26810  wlkeq  26938  wlkl1loop  26942  uspgr2wlkeq  26950  upgr2wlk  26972  redwlk  26980  wlkp1lem8  26988  usgr2wlkneq  27065  usgr2trlncl  27069  usgr2pthlem  27072  usgr2pth  27073  pthdlem1  27075  uspgrn2crct  27114  crctcshwlkn0lem7  27122  crctcshwlkn0  27127  wwlknp  27149  wwlksn0s  27167  wlkiswwlks1  27173  wlkiswwlks2lem4  27178  wlkiswwlksupgr2  27183  wlknewwlksn  27194  wwlksnred  27209  wwlksnredOLD  27210  wwlksnext  27211  rusgrnumwwlkl1  27304  clwwlkccatlem  27325  clwlkclwwlklem2a1  27328  clwlkclwwlklem2a  27334  clwlkclwwlklem3  27337  clwlkclwwlkf1lem3  27345  clwlkclwwlkf1lem3OLD  27346  clwwlkn  27371  clwwlknp  27382  clwwlkinwwlk  27385  clwwlkinwwlkOLD  27386  clwwlkn1  27387  clwwlkn2  27390  clwwlkel  27392  clwwlkfOLD  27393  clwwlkf  27398  clwwlkwwlksb  27406  wwlksext2clwwlk  27409  wwlksubclwwlk  27410  wwlksubclwwlkOLD  27411  clwlksfclwwlkOLD  27438  clwlksf1clwwlklemOLD  27444  clwwlknonex2  27480  1ewlk  27487  1wlkdlem4  27512  upgr3v3e3cycl  27552  upgr4cycl4dv4e  27557  dfconngr1  27560  isconngr1  27562  frgr3v  27652  frgrwopregasn  27693  frgrwopregbsn  27694  ubth  28280  acunirnmpt2  30005  acunirnmpt2f  30006  aciunf1  30008  lmxrge0  30539  sigaclcu3  30726  measval  30802  isrnmeas  30804  sitgval  30935  eulerpartlemsv3  30964  eulerpartlemo  30968  eulerpartlemn  30984  bnj1514  31673  subfacp1lem3  31706  subfacp1lem5  31708  txpconn  31756  cvxpconn  31766  cvmscbv  31782  cvmsi  31789  cvmsval  31790  elmrsubrn  31959  frpoinsg  32275  frinsg  32279  frrlem4  32317  bj-raldifsn  33572  poimirlem1  33949  poimirlem26  33974  poimirlem27  33975  poimirlem31  33979  poimirlem32  33980  heicant  33983  mblfinlem3  33987  ovoliunnfl  33990  voliunnfl  33992  volsupnfl  33993  cnicciblnc  34019  sdclem1  34076  fdc  34078  rrncmslem  34168  isass  34182  exidreslem  34213  exidresid  34215  isrngod  34234  isgrpda  34291  iscom2  34331  pautsetN  36168  tendofset  36828  tendoset  36829  hdmap14lem13  37950  kelac1  38471  gicabl  38507  lpirlnr  38525  fiinfi  38714  clsk1independent  39179  wessf1ornlem  40174  uzub  40447  mccl  40619  climsuse  40629  limsupmnfuzlem  40747  limsupmnfuz  40748  limsupre3uzlem  40756  limsupre3uz  40757  limsupreuz  40758  0cnv  40763  climuz  40765  lmbr3  40768  limsupgt  40799  liminflt  40826  xlimmnf  40856  xlimpnf  40857  xlimmnfmpt  40858  xlimpnfmpt  40859  dfxlim2  40863  fourierdlem2  41114  fourierdlem3  41115  fourierdlem31  41143  fourierdlem47  41158  fourierdlem70  41181  fourierdlem71  41182  fourierdlem73  41184  fourierdlem80  41191  fourierdlem103  41214  fourierdlem104  41215  fourierdlem113  41224  etransclem48  41287  etransc  41288  ismea  41453  caragenval  41495  omessle  41500  smfmullem2  41787  smfmul  41790  2ffzoeq  42220  iccpval  42233  iccpartigtl  42241  c0snmgmhm  42775  linds0  43115  lindsrng01  43118  rrx2line  43304