Theorem raleqi 3344

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

Syntax hints:   ↔ wb 205   = wceq 1541  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-ral 3070

This theorem is referenced by:  ralrab2  3637  ralprgf  4633  ralprg  4635  raltpg  4639  ralxp  5747  f12dfv  7139  f13dfv  7140  ralrnmpo  7403  ovmptss  7917  ixpfi2  9078  dffi3  9151  dfoi  9231  ssttrcl  9434  fseqenlem1  9764  kmlem12  9901  fzprval  13299  fztpval  13300  hashbc  14146  2prm  16378  prmreclem2  16599  xpsfrnel  17254  xpsle  17271  gsumwspan  18466  sgrp2rid2  18546  psgnunilem3  19085  pmtrsn  19108  islinds2  21001  ply1coe  21448  cply1coe0bi  21452  m2cpminvid2lem  21884  basdif0  22084  ordtbaslem  22320  ptbasfi  22713  ptcnplem  22753  ptrescn  22771  flftg  23128  ust0  23352  minveclem1  24569  minveclem3b  24573  minveclem6  24579  iblcnlem1  24933  ellimc2  25022  ftalem3  26205  dchreq  26387  pntlem3  26738  istrkg2ld  26802  istrkg3ld  26803  tgcgr4  26873  elntg2  27334  lfuhgr1v0e  27602  cplgr0  27773  wlkp1lem8  28028  usgr2pthlem  28110  pthdlem1  28113  pthd  28116  crctcshwlkn0  28165  2wlkdlem4  28272  2wlkdlem5  28273  2pthdlem1  28274  2wlkdlem10  28279  rusgrnumwwlkl1  28312  0ewlk  28457  0wlk  28459  wlk2v2elem2  28499  3wlkdlem4  28505  3wlkdlem5  28506  3pthdlem1  28507  3wlkdlem10  28512  minvecolem1  29215  minvecolem5  29222  minvecolem6  29223  cdj3lem3b  30781  prsiga  32078  hfext  34464  filnetlem4  34549  relowlssretop  35513  relowlpssretop  35514  elghomOLD  36024  iscrngo2  36134  refrelcoss3  36560  tendoset  38752  fnwe2lem2  40856  eliuniincex  42612  eliincex  42613  uzub  42925  liminflelimsuplem  43270  xlimbr  43322  subsaliuncl  43851  isomushgr  45230  rrx2pnecoorneor  46013  rrx2linest  46040