Theorem raleqi 3321

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

Syntax hints:   ↔ wb 209   = wceq 1570  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ral 3080  df-rex 3090

This theorem is referenced by:  ralrab2  3661  ralprgf  4660  ralprg  4662  raltpg  4664  ralxp  5827  f12dfv  7271  f13dfv  7272  ralrnmpo  7549  ovmptss  8084  ixpfi2  9303  dffi3  9387  dfoi  9469  ssttrcl  9680  fseqenlem1  10004  kmlem12  10141  fzprval  13609  fztpval  13610  hashbc  14486  2prm  16745  prmreclem2  16972  xpsfrnel  17611  xpsle  17628  s1chn  18671  chnub  18673  gsumwspan  18900  sgrp2rid2  18983  psgnunilem3  19561  pmtrsn  19584  islinds2  21963  ply1coe  22458  cply1coe0bi  22462  m2cpminvid2lem  22911  basdif0  23110  ordtbaslem  23345  ptbasfi  23738  ptcnplem  23778  ptrescn  23796  flftg  24153  ust0  24377  minveclem1  25583  minveclem3b  25587  minveclem6  25593  iblcnlem1  25947  ellimc2  26036  ftalem3  27239  dchreq  27422  pntlem3  27773  negbdaylem  28249  precsexlem9  28408  0reno  28689  1reno  28690  istrkg2ld  28729  istrkg3ld  28730  tgcgr4  28800  elntg2  29335  lfuhgr1v0e  29604  cplgr0  29775  wlkp1lem8  30028  usgr2pthlem  30112  pthdlem1  30115  pthd  30118  crctcshwlkn0  30170  2wlkdlem4  30277  2wlkdlem5  30278  2pthdlem1  30279  2wlkdlem10  30284  rusgrnumwwlkl1  30320  0ewlk  30465  0wlk  30467  wlk2v2elem2  30507  3wlkdlem4  30513  3wlkdlem5  30514  3pthdlem1  30515  3wlkdlem10  30520  minvecolem1  31226  minvecolem5  31233  minvecolem6  31234  cdj3lem3b  32792  elrgspnsubrunlem2  33568  prsiga  34521  hfext  36675  nmulrid  36689  filnetlem4  36912  mh-infprim2bi  37078  relowlssretop  38029  relowlpssretop  38030  elghomOLD  38558  iscrngo2  38668  refrelcoss3  39222  tendoset  41553  fnwe2lem2  43798  nadd1suc  44139  eliuniincex  45847  eliincex  45848  uzub  46165  liminflelimsuplem  46509  xlimbr  46561  subsaliuncl  47092  gricushgr  48702  isgrlim  48767  rrx2pnecoorneor  49515  rrx2linest  49542