Theorem raleqi 3296

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

Syntax hints:   ↔ wb 206   = wceq 1542  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ral 3053  df-rex 3063

This theorem is referenced by:  ralrab2  3658  ralprgf  4653  ralprg  4655  raltpg  4657  ralxp  5798  f12dfv  7229  f13dfv  7230  ralrnmpo  7507  ovmptss  8045  ixpfi2  9262  dffi3  9346  dfoi  9428  ssttrcl  9636  fseqenlem1  9946  kmlem12  10084  fzprval  13513  fztpval  13514  hashbc  14388  2prm  16631  prmreclem2  16857  xpsfrnel  17495  xpsle  17512  s1chn  18555  chnub  18557  gsumwspan  18783  sgrp2rid2  18866  psgnunilem3  19440  pmtrsn  19463  islinds2  21783  ply1coe  22257  cply1coe0bi  22261  m2cpminvid2lem  22713  basdif0  22912  ordtbaslem  23147  ptbasfi  23540  ptcnplem  23580  ptrescn  23598  flftg  23955  ust0  24179  minveclem1  25395  minveclem3b  25399  minveclem6  25405  iblcnlem1  25760  ellimc2  25849  ftalem3  27056  dchreq  27240  pntlem3  27591  negbdaylem  28067  precsexlem9  28226  0reno  28507  1reno  28508  istrkg2ld  28547  istrkg2ldOLD  28548  istrkg3ld  28549  tgcgr4  28619  elntg2  29074  lfuhgr1v0e  29343  cplgr0  29514  wlkp1lem8  29768  usgr2pthlem  29852  pthdlem1  29855  pthd  29858  crctcshwlkn0  29910  2wlkdlem4  30017  2wlkdlem5  30018  2pthdlem1  30019  2wlkdlem10  30024  rusgrnumwwlkl1  30060  0ewlk  30205  0wlk  30207  wlk2v2elem2  30247  3wlkdlem4  30253  3wlkdlem5  30254  3pthdlem1  30255  3wlkdlem10  30260  minvecolem1  30966  minvecolem5  30973  minvecolem6  30974  cdj3lem3b  32532  elrgspnsubrunlem2  33346  prsiga  34313  hfext  36403  filnetlem4  36601  relowlssretop  37622  relowlpssretop  37623  elghomOLD  38142  iscrngo2  38252  refrelcoss3  38808  tendoset  41139  fnwe2lem2  43412  nadd1suc  43753  eliuniincex  45472  eliincex  45473  uzub  45793  liminflelimsuplem  46137  xlimbr  46189  subsaliuncl  46720  gricushgr  48281  isgrlim  48346  rrx2pnecoorneor  49079  rrx2linest  49106