Theorem raleqi 3353

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

Syntax hints:   ↔ wb 198   = wceq 1658  ∀wral 3116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ral 3121

This theorem is referenced by:  ralrab2  3594  ralprg  4452  raltpg  4454  ralxp  5495  f12dfv  6783  f13dfv  6784  ralrnmpt2  7034  ovmptss  7521  ixpfi2  8532  dffi3  8605  dfoi  8684  fseqenlem1  9159  kmlem12  9297  fzprval  12694  fztpval  12695  hashbc  13525  2prm  15776  prmreclem2  15991  xpsfrnel  16575  xpsle  16593  gsumwspan  17736  sgrp2rid2  17766  psgnunilem3  18266  pmtrsn  18289  ply1coe  20025  cply1coe0bi  20029  islinds2  20518  m2cpminvid2lem  20928  basdif0  21127  ordtbaslem  21362  ptbasfi  21754  ptcnplem  21794  ptrescn  21812  flftg  22169  ust0  22392  minveclem1  23591  minveclem3b  23595  minveclem6  23601  iblcnlem1  23952  ellimc2  24039  ftalem3  25213  dchreq  25395  pntlem3  25710  istrkg2ld  25771  istrkg3ld  25772  elntg2  26283  lfuhgr1v0e  26550  cplgr0  26722  wlkp1lem8  26980  usgr2pthlem  27064  pthdlem1  27067  pthd  27070  crctcshwlkn0  27119  2wlkdlem4  27256  2wlkdlem5  27257  2pthdlem1  27258  2wlkdlem10  27263  rusgrnumwwlkl1  27296  0ewlk  27489  0wlk  27491  wlk2v2elem2  27531  3wlkdlem4  27537  3wlkdlem5  27538  3pthdlem1  27539  3wlkdlem10  27544  minvecolem1  28284  minvecolem5  28291  minvecolem6  28292  cdj3lem3b  29853  prsiga  30738  hfext  32828  filnetlem4  32913  relowlssretop  33755  relowlpssretop  33756  elghomOLD  34227  iscrngo2  34337  refrelcoss3  34760  tendoset  36833  fnwe2lem2  38463  eliuniincex  40106  eliincex  40107  uzub  40452  liminflelimsuplem  40801  xlimbr  40847  subsaliuncl  41366  isomushgr  42543  rrx2linest  43295