Theorem raleqi 3326

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 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

Syntax hints:   ↔ wb 198   = wceq 1653  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2778

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095

This theorem is referenced by:  ralrab2  3567  ralprg  4425  raltpg  4427  ralxp  5468  f12dfv  6758  f13dfv  6759  ralrnmpt2  7010  ovmptss  7496  ixpfi2  8507  dffi3  8580  dfoi  8659  fseqenlem1  9134  kmlem12  9272  fzprval  12654  fztpval  12655  hashbc  13485  2prm  15738  prmreclem2  15953  xpsfrnel  16537  xpsle  16555  gsumwspan  17698  sgrp2rid2  17728  psgnunilem3  18228  pmtrsn  18251  ply1coe  19987  cply1coe0bi  19991  islinds2  20476  m2cpminvid2lem  20886  basdif0  21085  ordtbaslem  21320  ptbasfi  21712  ptcnplem  21752  ptrescn  21770  flftg  22127  ust0  22350  minveclem1  23533  minveclem3b  23537  minveclem6  23543  iblcnlem1  23894  ellimc2  23981  ftalem3  25152  dchreq  25334  pntlem3  25649  istrkg2ld  25710  istrkg3ld  25711  lfuhgr1v0e  26487  cplgr0  26674  wlkp1lem8  26932  usgr2pthlem  27016  pthdlem1  27019  pthd  27022  crctcshwlkn0  27071  2wlkdlem4  27216  2wlkdlem5  27217  2pthdlem1  27218  2wlkdlem10  27223  rusgrnumwwlkl1  27258  0ewlk  27457  0wlk  27459  wlk2v2elem2  27499  3wlkdlem4  27505  3wlkdlem5  27506  3pthdlem1  27507  3wlkdlem10  27512  minvecolem1  28254  minvecolem5  28261  minvecolem6  28262  cdj3lem3b  29823  prsiga  30709  hfext  32802  filnetlem4  32887  relowlssretop  33708  relowlpssretop  33709  elghomOLD  34172  iscrngo2  34282  refrelcoss3  34706  tendoset  36779  fnwe2lem2  38401  eliuniincex  40045  eliincex  40046  uzub  40396  liminflelimsuplem  40746  xlimbr  40792  subsaliuncl  41314  isomushgr  42491