Theorem raleqi 3297

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 3296	. 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  3669  ralprgf  4658  ralprg  4660  raltpg  4662  ralxp  5805  f12dfv  7248  f13dfv  7249  ralrnmpo  7528  ovmptss  8072  ixpfi2  9301  dffi3  9382  dfoi  9464  ssttrcl  9668  fseqenlem1  9977  kmlem12  10115  fzprval  13546  fztpval  13547  hashbc  14418  2prm  16662  prmreclem2  16888  xpsfrnel  17525  xpsle  17542  gsumwspan  18773  sgrp2rid2  18853  psgnunilem3  19426  pmtrsn  19449  islinds2  21722  ply1coe  22185  cply1coe0bi  22189  m2cpminvid2lem  22641  basdif0  22840  ordtbaslem  23075  ptbasfi  23468  ptcnplem  23508  ptrescn  23526  flftg  23883  ust0  24107  minveclem1  25324  minveclem3b  25328  minveclem6  25334  iblcnlem1  25689  ellimc2  25778  ftalem3  26985  dchreq  27169  pntlem3  27520  negsbdaylem  27962  precsexlem9  28117  istrkg2ld  28387  istrkg3ld  28388  tgcgr4  28458  elntg2  28912  lfuhgr1v0e  29181  cplgr0  29352  wlkp1lem8  29608  usgr2pthlem  29693  pthdlem1  29696  pthd  29699  crctcshwlkn0  29751  2wlkdlem4  29858  2wlkdlem5  29859  2pthdlem1  29860  2wlkdlem10  29865  rusgrnumwwlkl1  29898  0ewlk  30043  0wlk  30045  wlk2v2elem2  30085  3wlkdlem4  30091  3wlkdlem5  30092  3pthdlem1  30093  3wlkdlem10  30098  minvecolem1  30803  minvecolem5  30810  minvecolem6  30811  cdj3lem3b  32369  s1chn  32936  chnub  32938  elrgspnsubrunlem2  33199  prsiga  34121  hfext  36171  filnetlem4  36369  relowlssretop  37351  relowlpssretop  37352  elghomOLD  37881  iscrngo2  37991  refrelcoss3  38454  tendoset  40753  fnwe2lem2  43040  nadd1suc  43381  eliuniincex  45103  eliincex  45104  uzub  45427  liminflelimsuplem  45773  xlimbr  45825  subsaliuncl  46356  gricushgr  47917  isgrlim  47981  rrx2pnecoorneor  48704  rrx2linest  48731