Theorem raleqi 3318

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ral 3078  df-rex 3088

This theorem is used by:  ralrab2  3656  ralprgf  4655  ralprg  4657  raltpg  4659  ralxp  5818  f12dfv  7281  f13dfv  7282  ralrnmpo  7559  ovmptss  8104  fnwe2lem3  8147  ixpfi2  9339  dffi3  9423  dfoi  9505  ssttrcl  9716  fseqenlem1  10103  kmlem12  10240  fzprval  13719  fztpval  13720  hashbc  14598  2prm  16867  prmreclem2  17095  xpsfrnel  17734  xpsle  17751  s1chn  18794  chnub  18796  gsumwspan  19042  sgrp2rid2  19125  psgnunilem3  19710  pmtrsn  19733  islinds2  22119  ply1coe  22616  cply1coe0bi  22620  m2cpminvid2lem  23072  basdif0  23271  ordtbaslem  23506  ptbasfi  23900  ptcnplem  23940  ptrescn  23958  flftg  24315  ust0  24539  minveclem1  25745  minveclem3b  25749  minveclem6  25755  iblcnlem1  26108  ellimc2  26197  ftalem3  27402  dchreq  27585  pntlem3  27936  negbdaylem  28442  precsexlem9  28601  0reno  28882  1reno  28883  istrkg2ld  28922  istrkg3ld  28923  tgcgr4  28994  elntg2  29563  lfuhgr1v0e  29835  cplgr0  30006  wlkp1lem8  30259  usgr2pthlem  30349  pthdlem1  30352  pthd  30355  crctcshwlkn0  30410  2wlkdlem4  30517  2wlkdlem5  30518  2pthdlem1  30519  2wlkdlem10  30524  rusgrnumwwlkl1  30560  0ewlk  30705  0wlk  30707  wlk2v2elem2  30757  3wlkdlem4  30763  3wlkdlem5  30764  3pthdlem1  30765  3wlkdlem10  30770  minvecolem1  31476  minvecolem5  31483  minvecolem6  31484  cdj3lem3b  33042  elrgspnsubrunlem2  33809  prsiga  34763  hfext  36934  nmulrid  36946  filnetlem4  37169  mh-infprim2bi  37335  relowlssretop  38286  relowlpssretop  38287  elghomOLD  38821  iscrngo2  38931  refrelcoss3  39485  tendoset  41816  nadd1suc  44393  eliuniincex  46123  eliincex  46124  uzub  46440  liminflelimsuplem  46784  xlimbr  46836  subsaliuncl  47367  gricushgr  49014  isgrlim  49079  rrx2pnecoorneor  49826  rrx2linest  49853