Theorem raleqi 3294

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 3293	. 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  3645  ralprgf  4639  ralprg  4641  raltpg  4643  ralxp  5791  f12dfv  7222  f13dfv  7223  ralrnmpo  7500  ovmptss  8037  ixpfi2  9254  dffi3  9338  dfoi  9420  ssttrcl  9630  fseqenlem1  9940  kmlem12  10078  fzprval  13533  fztpval  13534  hashbc  14409  2prm  16655  prmreclem2  16882  xpsfrnel  17520  xpsle  17537  s1chn  18580  chnub  18582  gsumwspan  18808  sgrp2rid2  18891  psgnunilem3  19465  pmtrsn  19488  islinds2  21806  ply1coe  22276  cply1coe0bi  22280  m2cpminvid2lem  22732  basdif0  22931  ordtbaslem  23166  ptbasfi  23559  ptcnplem  23599  ptrescn  23617  flftg  23974  ust0  24198  minveclem1  25404  minveclem3b  25408  minveclem6  25414  iblcnlem1  25768  ellimc2  25857  ftalem3  27055  dchreq  27238  pntlem3  27589  negbdaylem  28065  precsexlem9  28224  0reno  28505  1reno  28506  istrkg2ld  28545  istrkg3ld  28546  tgcgr4  28616  elntg2  29071  lfuhgr1v0e  29340  cplgr0  29511  wlkp1lem8  29765  usgr2pthlem  29849  pthdlem1  29852  pthd  29855  crctcshwlkn0  29907  2wlkdlem4  30014  2wlkdlem5  30015  2pthdlem1  30016  2wlkdlem10  30021  rusgrnumwwlkl1  30057  0ewlk  30202  0wlk  30204  wlk2v2elem2  30244  3wlkdlem4  30250  3wlkdlem5  30251  3pthdlem1  30252  3wlkdlem10  30257  minvecolem1  30963  minvecolem5  30970  minvecolem6  30971  cdj3lem3b  32529  elrgspnsubrunlem2  33327  prsiga  34294  hfext  36384  filnetlem4  36582  mh-infprim2bi  36748  relowlssretop  37696  relowlpssretop  37697  elghomOLD  38225  iscrngo2  38335  refrelcoss3  38891  tendoset  41222  fnwe2lem2  43500  nadd1suc  43841  eliuniincex  45560  eliincex  45561  uzub  45880  liminflelimsuplem  46224  xlimbr  46276  subsaliuncl  46807  gricushgr  48408  isgrlim  48473  rrx2pnecoorneor  49206  rrx2linest  49233