Theorem raleqi 3362

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

Syntax hints:   ↔ wb 209   = wceq 1538  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111

This theorem is referenced by:  ralrab2  3638  ralprgf  4590  raltpg  4594  ralxp  5676  f12dfv  7008  f13dfv  7009  ralrnmpo  7268  ovmptss  7771  ixpfi2  8806  dffi3  8879  dfoi  8959  fseqenlem1  9435  kmlem12  9572  fzprval  12963  fztpval  12964  hashbc  13807  2prm  16026  prmreclem2  16243  xpsfrnel  16827  xpsle  16844  gsumwspan  18003  sgrp2rid2  18083  psgnunilem3  18616  pmtrsn  18639  islinds2  20502  ply1coe  20925  cply1coe0bi  20929  m2cpminvid2lem  21359  basdif0  21558  ordtbaslem  21793  ptbasfi  22186  ptcnplem  22226  ptrescn  22244  flftg  22601  ust0  22825  minveclem1  24028  minveclem3b  24032  minveclem6  24038  iblcnlem1  24391  ellimc2  24480  ftalem3  25660  dchreq  25842  pntlem3  26193  istrkg2ld  26254  istrkg3ld  26255  tgcgr4  26325  elntg2  26779  lfuhgr1v0e  27044  cplgr0  27215  wlkp1lem8  27470  usgr2pthlem  27552  pthdlem1  27555  pthd  27558  crctcshwlkn0  27607  2wlkdlem4  27714  2wlkdlem5  27715  2pthdlem1  27716  2wlkdlem10  27721  rusgrnumwwlkl1  27754  0ewlk  27899  0wlk  27901  wlk2v2elem2  27941  3wlkdlem4  27947  3wlkdlem5  27948  3pthdlem1  27949  3wlkdlem10  27954  minvecolem1  28657  minvecolem5  28664  minvecolem6  28665  cdj3lem3b  30223  prsiga  31500  hfext  33757  filnetlem4  33842  relowlssretop  34780  relowlpssretop  34781  elghomOLD  35325  iscrngo2  35435  refrelcoss3  35863  tendoset  38055  fnwe2lem2  39995  eliuniincex  41745  eliincex  41746  uzub  42068  liminflelimsuplem  42417  xlimbr  42469  subsaliuncl  42998  isomushgr  44344  rrx2pnecoorneor  45129  rrx2linest  45156