Theorem raleqi 3293

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

Syntax hints:   ↔ wb 206   = wceq 1542  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  ralrab2  3644  ralprgf  4638  ralprg  4640  raltpg  4642  ralxp  5796  f12dfv  7228  f13dfv  7229  ralrnmpo  7506  ovmptss  8043  ixpfi2  9260  dffi3  9344  dfoi  9426  ssttrcl  9636  fseqenlem1  9946  kmlem12  10084  fzprval  13539  fztpval  13540  hashbc  14415  2prm  16661  prmreclem2  16888  xpsfrnel  17526  xpsle  17543  s1chn  18586  chnub  18588  gsumwspan  18814  sgrp2rid2  18897  psgnunilem3  19471  pmtrsn  19494  islinds2  21793  ply1coe  22263  cply1coe0bi  22267  m2cpminvid2lem  22719  basdif0  22918  ordtbaslem  23153  ptbasfi  23546  ptcnplem  23586  ptrescn  23604  flftg  23961  ust0  24185  minveclem1  25391  minveclem3b  25395  minveclem6  25401  iblcnlem1  25755  ellimc2  25844  ftalem3  27038  dchreq  27221  pntlem3  27572  negbdaylem  28048  precsexlem9  28207  0reno  28488  1reno  28489  istrkg2ld  28528  istrkg3ld  28529  tgcgr4  28599  elntg2  29054  lfuhgr1v0e  29323  cplgr0  29494  wlkp1lem8  29747  usgr2pthlem  29831  pthdlem1  29834  pthd  29837  crctcshwlkn0  29889  2wlkdlem4  29996  2wlkdlem5  29997  2pthdlem1  29998  2wlkdlem10  30003  rusgrnumwwlkl1  30039  0ewlk  30184  0wlk  30186  wlk2v2elem2  30226  3wlkdlem4  30232  3wlkdlem5  30233  3pthdlem1  30234  3wlkdlem10  30239  minvecolem1  30945  minvecolem5  30952  minvecolem6  30953  cdj3lem3b  32511  elrgspnsubrunlem2  33309  prsiga  34275  hfext  36365  filnetlem4  36563  mh-infprim2bi  36729  relowlssretop  37679  relowlpssretop  37680  elghomOLD  38208  iscrngo2  38318  refrelcoss3  38874  tendoset  41205  fnwe2lem2  43479  nadd1suc  43820  eliuniincex  45539  eliincex  45540  uzub  45859  liminflelimsuplem  46203  xlimbr  46255  subsaliuncl  46786  gricushgr  48393  isgrlim  48458  rrx2pnecoorneor  49191  rrx2linest  49218