Theorem raleqi 3287

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 3286	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  ralrab2  3658  ralprgf  4646  ralprg  4648  raltpg  4650  ralxp  5784  f12dfv  7210  f13dfv  7211  ralrnmpo  7488  ovmptss  8026  ixpfi2  9240  dffi3  9321  dfoi  9403  ssttrcl  9611  fseqenlem1  9918  kmlem12  10056  fzprval  13488  fztpval  13489  hashbc  14360  2prm  16603  prmreclem2  16829  xpsfrnel  17466  xpsle  17483  gsumwspan  18720  sgrp2rid2  18800  psgnunilem3  19375  pmtrsn  19398  islinds2  21720  ply1coe  22183  cply1coe0bi  22187  m2cpminvid2lem  22639  basdif0  22838  ordtbaslem  23073  ptbasfi  23466  ptcnplem  23506  ptrescn  23524  flftg  23881  ust0  24105  minveclem1  25322  minveclem3b  25326  minveclem6  25332  iblcnlem1  25687  ellimc2  25776  ftalem3  26983  dchreq  27167  pntlem3  27518  negsbdaylem  27967  precsexlem9  28122  istrkg2ld  28405  istrkg3ld  28406  tgcgr4  28476  elntg2  28930  lfuhgr1v0e  29199  cplgr0  29370  wlkp1lem8  29624  usgr2pthlem  29708  pthdlem1  29711  pthd  29714  crctcshwlkn0  29766  2wlkdlem4  29873  2wlkdlem5  29874  2pthdlem1  29875  2wlkdlem10  29880  rusgrnumwwlkl1  29913  0ewlk  30058  0wlk  30060  wlk2v2elem2  30100  3wlkdlem4  30106  3wlkdlem5  30107  3pthdlem1  30108  3wlkdlem10  30113  minvecolem1  30818  minvecolem5  30825  minvecolem6  30826  cdj3lem3b  32384  s1chn  32953  chnub  32955  elrgspnsubrunlem2  33189  prsiga  34104  hfext  36167  filnetlem4  36365  relowlssretop  37347  relowlpssretop  37348  elghomOLD  37877  iscrngo2  37987  refrelcoss3  38450  tendoset  40748  fnwe2lem2  43034  nadd1suc  43375  eliuniincex  45097  eliincex  45098  uzub  45420  liminflelimsuplem  45766  xlimbr  45818  subsaliuncl  46349  gricushgr  47911  isgrlim  47976  rrx2pnecoorneor  48710  rrx2linest  48737