Theorem raleqi 3290

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

Syntax hints:   ↔ wb 206   = wceq 1541  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ral 3048  df-rex 3057

This theorem is referenced by:  ralrab2  3652  ralprgf  4644  ralprg  4646  raltpg  4648  ralxp  5780  f12dfv  7207  f13dfv  7208  ralrnmpo  7485  ovmptss  8023  ixpfi2  9234  dffi3  9315  dfoi  9397  ssttrcl  9605  fseqenlem1  9915  kmlem12  10053  fzprval  13485  fztpval  13486  hashbc  14360  2prm  16603  prmreclem2  16829  xpsfrnel  17466  xpsle  17483  s1chn  18526  chnub  18528  gsumwspan  18754  sgrp2rid2  18834  psgnunilem3  19408  pmtrsn  19431  islinds2  21750  ply1coe  22213  cply1coe0bi  22217  m2cpminvid2lem  22669  basdif0  22868  ordtbaslem  23103  ptbasfi  23496  ptcnplem  23536  ptrescn  23554  flftg  23911  ust0  24135  minveclem1  25351  minveclem3b  25355  minveclem6  25361  iblcnlem1  25716  ellimc2  25805  ftalem3  27012  dchreq  27196  pntlem3  27547  negsbdaylem  27998  precsexlem9  28153  istrkg2ld  28438  istrkg3ld  28439  tgcgr4  28509  elntg2  28963  lfuhgr1v0e  29232  cplgr0  29403  wlkp1lem8  29657  usgr2pthlem  29741  pthdlem1  29744  pthd  29747  crctcshwlkn0  29799  2wlkdlem4  29906  2wlkdlem5  29907  2pthdlem1  29908  2wlkdlem10  29913  rusgrnumwwlkl1  29949  0ewlk  30094  0wlk  30096  wlk2v2elem2  30136  3wlkdlem4  30142  3wlkdlem5  30143  3pthdlem1  30144  3wlkdlem10  30149  minvecolem1  30854  minvecolem5  30861  minvecolem6  30862  cdj3lem3b  32420  elrgspnsubrunlem2  33215  prsiga  34144  hfext  36227  filnetlem4  36425  relowlssretop  37407  relowlpssretop  37408  elghomOLD  37937  iscrngo2  38047  refrelcoss3  38575  tendoset  40868  fnwe2lem2  43154  nadd1suc  43495  eliuniincex  45216  eliincex  45217  uzub  45539  liminflelimsuplem  45883  xlimbr  45935  subsaliuncl  46466  gricushgr  48027  isgrlim  48092  rrx2pnecoorneor  48826  rrx2linest  48853