Theorem raleqi 3299

Description: Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
raleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
raleqi	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleqi

Step	Hyp	Ref	Expression
1		raleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		raleq 3298	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

Syntax hints:   ↔ wb 206   = wceq 1540  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ral 3046  df-rex 3055

This theorem is referenced by:  ralrab2  3671  ralprgf  4660  ralprg  4662  raltpg  4664  ralxp  5807  f12dfv  7250  f13dfv  7251  ralrnmpo  7530  ovmptss  8074  ixpfi2  9307  dffi3  9388  dfoi  9470  ssttrcl  9674  fseqenlem1  9983  kmlem12  10121  fzprval  13552  fztpval  13553  hashbc  14424  2prm  16668  prmreclem2  16894  xpsfrnel  17531  xpsle  17548  gsumwspan  18779  sgrp2rid2  18859  psgnunilem3  19432  pmtrsn  19455  islinds2  21728  ply1coe  22191  cply1coe0bi  22195  m2cpminvid2lem  22647  basdif0  22846  ordtbaslem  23081  ptbasfi  23474  ptcnplem  23514  ptrescn  23532  flftg  23889  ust0  24113  minveclem1  25330  minveclem3b  25334  minveclem6  25340  iblcnlem1  25695  ellimc2  25784  ftalem3  26991  dchreq  27175  pntlem3  27526  negsbdaylem  27968  precsexlem9  28123  istrkg2ld  28393  istrkg3ld  28394  tgcgr4  28464  elntg2  28918  lfuhgr1v0e  29187  cplgr0  29358  wlkp1lem8  29614  usgr2pthlem  29699  pthdlem1  29702  pthd  29705  crctcshwlkn0  29757  2wlkdlem4  29864  2wlkdlem5  29865  2pthdlem1  29866  2wlkdlem10  29871  rusgrnumwwlkl1  29904  0ewlk  30049  0wlk  30051  wlk2v2elem2  30091  3wlkdlem4  30097  3wlkdlem5  30098  3pthdlem1  30099  3wlkdlem10  30104  minvecolem1  30809  minvecolem5  30816  minvecolem6  30817  cdj3lem3b  32375  s1chn  32942  chnub  32944  elrgspnsubrunlem2  33205  prsiga  34127  hfext  36166  filnetlem4  36364  relowlssretop  37346  relowlpssretop  37347  elghomOLD  37876  iscrngo2  37986  refrelcoss3  38449  tendoset  40748  fnwe2lem2  43033  nadd1suc  43374  eliuniincex  45096  eliincex  45097  uzub  45420  liminflelimsuplem  45766  xlimbr  45818  subsaliuncl  46349  gricushgr  47907  isgrlim  47971  rrx2pnecoorneor  48694  rrx2linest  48721