Theorem raleqi 3317

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ral 3077  df-rex 3087

This theorem is used by:  ralrab2  3656  ralprgf  4655  ralprg  4657  raltpg  4659  ralxp  5821  f12dfv  7275  f13dfv  7276  ralrnmpo  7553  ovmptss  8091  ixpfi2  9320  dffi3  9404  dfoi  9486  ssttrcl  9697  fseqenlem1  10030  kmlem12  10167  fzprval  13643  fztpval  13644  hashbc  14521  2prm  16785  prmreclem2  17012  xpsfrnel  17651  xpsle  17668  s1chn  18711  chnub  18713  gsumwspan  18958  sgrp2rid2  19041  psgnunilem3  19626  pmtrsn  19649  islinds2  22029  ply1coe  22526  cply1coe0bi  22530  m2cpminvid2lem  22982  basdif0  23181  ordtbaslem  23416  ptbasfi  23810  ptcnplem  23850  ptrescn  23868  flftg  24225  ust0  24449  minveclem1  25655  minveclem3b  25659  minveclem6  25665  iblcnlem1  26018  ellimc2  26107  ftalem3  27314  dchreq  27497  pntlem3  27848  negbdaylem  28324  precsexlem9  28483  0reno  28764  1reno  28765  istrkg2ld  28804  istrkg3ld  28805  tgcgr4  28876  elntg2  29445  lfuhgr1v0e  29717  cplgr0  29888  wlkp1lem8  30141  usgr2pthlem  30231  pthdlem1  30234  pthd  30237  crctcshwlkn0  30292  2wlkdlem4  30399  2wlkdlem5  30400  2pthdlem1  30401  2wlkdlem10  30406  rusgrnumwwlkl1  30442  0ewlk  30587  0wlk  30589  wlk2v2elem2  30639  3wlkdlem4  30645  3wlkdlem5  30646  3pthdlem1  30647  3wlkdlem10  30652  minvecolem1  31358  minvecolem5  31365  minvecolem6  31366  cdj3lem3b  32924  elrgspnsubrunlem2  33691  prsiga  34644  hfext  36766  nmulrid  36780  filnetlem4  37003  mh-infprim2bi  37169  relowlssretop  38120  relowlpssretop  38121  elghomOLD  38640  iscrngo2  38750  refrelcoss3  39304  tendoset  41635  fnwe2lem2  43895  nadd1suc  44236  eliuniincex  45944  eliincex  45945  uzub  46262  liminflelimsuplem  46606  xlimbr  46658  subsaliuncl  47189  gricushgr  48836  isgrlim  48901  rrx2pnecoorneor  49648  rrx2linest  49675