Theorem raleqdv 3323

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ral 3081  df-rex 3091

This theorem is used by:  raleqtrdv  3325  raleqtrrdv  3327  raleqbidva  3329  raldifeq  4452  frpoinsg  6361  f12dfv  7301  f13dfv  7302  cbvfo  7317  isoselem  7369  ofrfvalg  7722  omsinds  7919  frpoins3xpg  8181  frpoins3xp3g  8182  frrlem4  8332  issmo2  8382  smoeq  8383  on2ind  8703  on3ind  8704  naddsuc2  8736  frfi  9301  marypha1lem  9449  marypha1  9450  dfoi  9529  oieq2  9531  ordtypecbv  9535  ordtypelem2  9537  ordtypelem3  9538  ordtypelem9  9544  wemapwe  9722  ttrclss  9745  ttrclselem2  9751  frinsg  9779  tcrank  9925  scotteqd  9954  isacn  10147  pwsdompw  10305  isfin2  10396  isfin3ds  10431  isf33lem  10468  hsmexlem4  10531  zorn2lem6  10603  zorn2lem7  10604  zorn2g  10605  fpwwe2lem12  10751  uzsupss  13091  fzrevral2  13771  fzrevral3  13772  fzshftral  13773  fzoshftral  13946  uzsinds  14154  expmulnbnd  14403  eqs1  14785  swrdspsleq  14840  pfxeq  14870  pfxsuffeqwrdeq  14872  repswsymballbi  14956  cshw1  14998  pfx2  15124  wwlktovf1  15136  eqwrds3  15140  rexuz3  15542  rexuzre  15546  limsupgle  15670  rlim  15688  climconst  15736  rlimclim1  15738  climshftlem  15767  isercoll  15861  caucvgb  15873  serf0  15874  mertenslem1  16079  coprmprod  16862  coprmproddvds  16864  prmind2  16886  vdwlem10  17194  vdwlem13  17197  vdwnnlem2  17200  vdwnnlem3  17201  vdwnn  17202  ramval  17212  ramz  17229  prmgaplem5  17259  isacs  17851  cidpropd  17910  monpropd  17938  isssc  18021  fullsubc  18051  funcpropd  18103  isfth  18117  fthpropd  18124  grpidpropd  18868  sgrppropd  18946  mndpropd  18977  nmznsg  19404  ghmnsgima  19480  symgextfo  19663  gsmsymgrfixlem1  19668  gsmsymgrfix  19669  fvcosymgeq  19670  gsmsymgreqlem2  19672  psgnunilem3  19737  sylow2blem3  19863  sylow3lem6  19873  cmnpropd  20032  telgsumfzs  20230  rngpropd  20423  ringpropd  20546  c0snmgmhm  20719  abvpropd  21119  lsspropd  21319  lmhmpropd  21375  lbspropd  21401  pj1lmhm  21402  psgndiflemB  21933  phlpropd  21988  islindf  22145  lindfmm  22160  islindf4  22171  islindf5  22172  assapropd  22206  scmatf1  22873  isclo  23432  lmfval  23577  lmconst  23606  iscnrm2  23683  ist0-2  23689  ist1-2  23692  ishaus2  23696  subislly  23827  elpt  23918  elptr  23919  ptbasfi  23927  fclscmp  24376  ufilcmp  24378  cnpfcf  24387  alexsubALTlem1  24393  alexsubALTlem2  24394  alexsubALTlem4  24396  tmdgsum2  24442  tsmsf1o  24491  ustval  24549  ucnval  24622  imasdsf1olem  24719  imasf1oxmet  24721  imasf1omet  24722  metss  24854  prdsxmslem2  24875  lebnumlem3  25311  ishtpy  25320  lmnn  25611  evthicc  25807  cniccbdd  25809  ovolicc2lem4  25868  0pledm  26021  cniccibl  26188  cnicciblnc  26190  c1lip1  26344  lhop1  26361  itgsubstlem  26395  ulmshftlem  26743  ulm0  26745  ulmcau  26749  rlimcnp  27320  fsumdvdsmul  27549  chtub  27566  2sqlem10  27782  dchrisum0flb  27864  pntpbnd1  27940  pntpbnd  27942  pntibndlem2  27945  pntibndlem3  27946  pntibnd  27947  pntlemi  27958  pntleme  27962  pntlem3  27963  pntlemp  27964  pntleml  27965  pnt3  27966  madebdaylemlrcut  28312  noinds  28358  no2indlesm  28367  no3inds  28371  precsexlem9  28628  istrkgld  28948  trgcgrg  29005  tgcgr4  29021  isperp  29214  brbtwn  29504  usgruspgrb  29791  nbgr2vtx1edg  29958  nbuhgr2vtx1edgb  29960  nbgr1vtx  29966  uvtx01vtx  30005  cplgr1v  30038  wlkeq  30241  wlkl1loop  30245  uspgr2wlkeq  30253  upgr2wlk  30274  redwlk  30278  wlkp1lem8  30286  usgr2wlkneq  30369  usgr2trlncl  30373  usgr2pthlem  30376  usgr2pth  30377  pthdlem1  30379  uspgrn2crct  30424  crctcshwlkn0  30437  wwlknp  30459  wwlksn0s  30477  wlkiswwlks1  30483  wlkiswwlks2lem4  30488  wwlksnred  30508  rusgrnumwwlkl1  30587  clwwlkccatlem  30607  clwlkclwwlklem2a1  30610  clwlkclwwlklem2a  30616  clwlkclwwlklem3  30619  clwwlkn  30644  clwwlknp  30655  clwwlkinwwlk  30658  clwwlkn1  30659  clwwlkn2  30662  clwwlkel  30664  clwwlkf  30665  clwwlkwwlksb  30672  1ewlk  30733  upgr3v3e3cycl  30808  upgr4cycl4dv4e  30813  dfconngr1  30816  isconngr1  30818  frgr3v  30903  frgrwopregasn  30944  frgrwopregbsn  30945  ubth  31502  aciunf1  33326  fnpreimac  33333  fxpgaval  33795  crngmxidl  34061  lmxrge0  34651  measval  34898  isrnmeas  34900  sitgval  35031  eulerpartlemo  35064  eulerpartlemn  35080  onvf1odlem4  36033  subfacp1lem3  36113  subfacp1lem5  36115  txpconn  36163  cvxpconn  36173  cvmscbv  36189  cvmsi  36196  cvmsval  36197  satf  36284  sat1el2xp  36310  elmrsubrn  36451  weiunlem  37428  bj-raldifsn  38211  poimirlem26  38755  poimirlem27  38756  poimirlem31  38760  poimirlem32  38761  heicant  38764  mblfinlem3  38768  ovoliunnfl  38771  voliunnfl  38773  volsupnfl  38774  sdclem1  38868  fdc  38870  rrncmslem  38957  isass  38971  isrngod  39023  isgrpda  39080  iscom2  39120  pautsetN  41346  tendofset  42006  tendoset  42007  hdmap14lem13  43128  3factsumint1  43262  sticksstones3  43389  kelac1  44256  gicabl  44292  cantnfresb  44516  safesnsupfilb  44609  fiinfi  44764  clsk1independent  45236  wessf1ornlem  46403  uzub  46644  rexanuz2nf  46705  mccl  46813  climsuse  46823  limsupmnfuzlem  46939  limsupmnfuz  46940  limsupre3uzlem  46948  limsupre3uz  46949  limsupreuz  46950  0cnv  46955  climuz  46957  lmbr3  46960  limsupgt  46991  liminflt  47018  xlimpnfxnegmnf  47027  xlimmnf  47054  xlimpnf  47055  xlimmnfmpt  47056  xlimpnfmpt  47057  dfxlim2  47061  fourierdlem2  47322  fourierdlem3  47323  fourierdlem31  47351  fourierdlem47  47366  fourierdlem70  47389  fourierdlem71  47390  fourierdlem80  47399  fourierdlem103  47422  fourierdlem104  47423  fourierdlem113  47432  etransclem48  47495  etransc  47496  caragenval  47706  omessle  47711  smfmullem2  48005  smfmul  48008  2ffzoeq  48601  iccpval  48700  iccpartigtl  48708  nprmmul1  48812  cycl3grtrilem  49247  grlimedgclnbgr  49296  grlimgrtri  49304  grilcbri2  49312  usgrexmpl2trifr  49338  gpg5nbgrvtx03star  49381  gpg5nbgr3star  49382  lindsrng01  49783  rrx2line  50055  initopropd  50568  termopropd  50569  fucofulem2  50636  thincpropd  50780  isinito2lem  50836