Theorem raleqi 3323

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

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

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ral 3082  df-rex 3092

This theorem is used by:  ralrab2  3663  ralprgf  4662  ralprg  4664  raltpg  4666  ralxp  5829  f12dfv  7280  f13dfv  7281  ralrnmpo  7558  ovmptss  8094  ixpfi2  9314  dffi3  9398  dfoi  9480  ssttrcl  9691  fseqenlem1  10024  kmlem12  10161  fzprval  13632  fztpval  13633  hashbc  14510  2prm  16774  prmreclem2  17001  xpsfrnel  17640  xpsle  17657  s1chn  18700  chnub  18702  gsumwspan  18944  sgrp2rid2  19027  psgnunilem3  19612  pmtrsn  19635  islinds2  22015  ply1coe  22510  cply1coe0bi  22514  m2cpminvid2lem  22963  basdif0  23162  ordtbaslem  23397  ptbasfi  23791  ptcnplem  23831  ptrescn  23849  flftg  24206  ust0  24430  minveclem1  25636  minveclem3b  25640  minveclem6  25646  iblcnlem1  26000  ellimc2  26089  ftalem3  27292  dchreq  27475  pntlem3  27826  negbdaylem  28302  precsexlem9  28461  0reno  28742  1reno  28743  istrkg2ld  28782  istrkg3ld  28783  tgcgr4  28853  elntg2  29392  lfuhgr1v0e  29664  cplgr0  29835  wlkp1lem8  30088  usgr2pthlem  30178  pthdlem1  30181  pthd  30184  crctcshwlkn0  30239  2wlkdlem4  30346  2wlkdlem5  30347  2pthdlem1  30348  2wlkdlem10  30353  rusgrnumwwlkl1  30389  0ewlk  30534  0wlk  30536  wlk2v2elem2  30580  3wlkdlem4  30586  3wlkdlem5  30587  3pthdlem1  30588  3wlkdlem10  30593  minvecolem1  31299  minvecolem5  31306  minvecolem6  31307  cdj3lem3b  32865  elrgspnsubrunlem2  33634  prsiga  34587  hfext  36714  nmulrid  36728  filnetlem4  36951  mh-infprim2bi  37117  relowlssretop  38068  relowlpssretop  38069  elghomOLD  38598  iscrngo2  38708  refrelcoss3  39262  tendoset  41593  fnwe2lem2  43838  nadd1suc  44179  eliuniincex  45887  eliincex  45888  uzub  46205  liminflelimsuplem  46549  xlimbr  46601  subsaliuncl  47132  gricushgr  48742  isgrlim  48807  rrx2pnecoorneor  49554  rrx2linest  49581