Theorem raleqi 3307

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ral 3053  df-rex 3062

This theorem is referenced by:  ralrab2  3686  ralprgf  4675  ralprg  4677  raltpg  4679  ralxp  5826  f12dfv  7271  f13dfv  7272  ralrnmpo  7551  ovmptss  8097  ixpfi2  9367  dffi3  9448  dfoi  9530  ssttrcl  9734  fseqenlem1  10043  kmlem12  10181  fzprval  13607  fztpval  13608  hashbc  14476  2prm  16716  prmreclem2  16942  xpsfrnel  17581  xpsle  17598  gsumwspan  18829  sgrp2rid2  18909  psgnunilem3  19482  pmtrsn  19505  islinds2  21778  ply1coe  22241  cply1coe0bi  22245  m2cpminvid2lem  22697  basdif0  22896  ordtbaslem  23131  ptbasfi  23524  ptcnplem  23564  ptrescn  23582  flftg  23939  ust0  24163  minveclem1  25381  minveclem3b  25385  minveclem6  25391  iblcnlem1  25746  ellimc2  25835  ftalem3  27042  dchreq  27226  pntlem3  27577  negsbdaylem  28019  precsexlem9  28174  istrkg2ld  28444  istrkg3ld  28445  tgcgr4  28515  elntg2  28969  lfuhgr1v0e  29238  cplgr0  29409  wlkp1lem8  29665  usgr2pthlem  29750  pthdlem1  29753  pthd  29756  crctcshwlkn0  29808  2wlkdlem4  29915  2wlkdlem5  29916  2pthdlem1  29917  2wlkdlem10  29922  rusgrnumwwlkl1  29955  0ewlk  30100  0wlk  30102  wlk2v2elem2  30142  3wlkdlem4  30148  3wlkdlem5  30149  3pthdlem1  30150  3wlkdlem10  30155  minvecolem1  30860  minvecolem5  30867  minvecolem6  30868  cdj3lem3b  32426  s1chn  32995  chnub  32997  elrgspnsubrunlem2  33248  prsiga  34167  hfext  36206  filnetlem4  36404  relowlssretop  37386  relowlpssretop  37387  elghomOLD  37916  iscrngo2  38026  refrelcoss3  38486  tendoset  40783  fnwe2lem2  43050  nadd1suc  43391  eliuniincex  45113  eliincex  45114  uzub  45438  liminflelimsuplem  45784  xlimbr  45836  subsaliuncl  46367  gricushgr  47910  isgrlim  47974  rrx2pnecoorneor  48675  rrx2linest  48702