Theorem raleqi 3327

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

Syntax hints:   ↔ wb 209   = wceq 1567  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ral 3086  df-rex 3096

This theorem is referenced by:  ralrab2  3670  ralprgf  4665  ralprg  4667  raltpg  4669  ralxp  5828  f12dfv  7272  f13dfv  7273  ralrnmpo  7550  ovmptss  8088  ixpfi2  9307  dffi3  9391  dfoi  9473  ssttrcl  9684  fseqenlem1  10008  kmlem12  10145  fzprval  13613  fztpval  13614  hashbc  14490  2prm  16750  prmreclem2  16977  xpsfrnel  17616  xpsle  17633  s1chn  18676  chnub  18678  gsumwspan  18905  sgrp2rid2  18988  psgnunilem3  19566  pmtrsn  19589  islinds2  21932  ply1coe  22427  cply1coe0bi  22431  m2cpminvid2lem  22880  basdif0  23079  ordtbaslem  23314  ptbasfi  23707  ptcnplem  23747  ptrescn  23765  flftg  24122  ust0  24346  minveclem1  25552  minveclem3b  25556  minveclem6  25562  iblcnlem1  25916  ellimc2  26005  ftalem3  27205  dchreq  27388  pntlem3  27739  negbdaylem  28215  precsexlem9  28374  0reno  28655  1reno  28656  istrkg2ld  28695  istrkg3ld  28696  tgcgr4  28766  elntg2  29276  lfuhgr1v0e  29545  cplgr0  29716  wlkp1lem8  29969  usgr2pthlem  30053  pthdlem1  30056  pthd  30059  crctcshwlkn0  30111  2wlkdlem4  30218  2wlkdlem5  30219  2pthdlem1  30220  2wlkdlem10  30225  rusgrnumwwlkl1  30261  0ewlk  30406  0wlk  30408  wlk2v2elem2  30448  3wlkdlem4  30454  3wlkdlem5  30455  3pthdlem1  30456  3wlkdlem10  30461  minvecolem1  31167  minvecolem5  31174  minvecolem6  31175  cdj3lem3b  32733  elrgspnsubrunlem2  33509  prsiga  34466  hfext  36574  filnetlem4  36781  mh-infprim2bi  36947  relowlssretop  37897  relowlpssretop  37898  elghomOLD  38426  iscrngo2  38536  refrelcoss3  39092  tendoset  41423  fnwe2lem2  43670  nadd1suc  44011  eliuniincex  45719  eliincex  45720  uzub  46037  liminflelimsuplem  46381  xlimbr  46433  subsaliuncl  46964  gricushgr  48571  isgrlim  48636  rrx2pnecoorneor  49380  rrx2linest  49407