Theorem raleqi 3322

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

Syntax hints:   ↔ wb 205   = wceq 1541  ∀wral 3060

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ral 3061  df-rex 3070

This theorem is referenced by:  ralrab2  3690  ralprgf  4689  ralprg  4691  raltpg  4695  ralxp  5833  f12dfv  7255  f13dfv  7256  ralrnmpo  7530  ovmptss  8061  ixpfi2  9333  dffi3  9408  dfoi  9488  ssttrcl  9692  fseqenlem1  10001  kmlem12  10138  fzprval  13544  fztpval  13545  hashbc  14394  2prm  16611  prmreclem2  16832  xpsfrnel  17490  xpsle  17507  gsumwspan  18702  sgrp2rid2  18782  psgnunilem3  19328  pmtrsn  19351  islinds2  21301  ply1coe  21749  cply1coe0bi  21753  m2cpminvid2lem  22185  basdif0  22385  ordtbaslem  22621  ptbasfi  23014  ptcnplem  23054  ptrescn  23072  flftg  23429  ust0  23653  minveclem1  24870  minveclem3b  24874  minveclem6  24880  iblcnlem1  25234  ellimc2  25323  ftalem3  26506  dchreq  26688  pntlem3  27039  negsbdaylem  27444  istrkg2ld  27576  istrkg3ld  27577  tgcgr4  27647  elntg2  28108  lfuhgr1v0e  28376  cplgr0  28547  wlkp1lem8  28802  usgr2pthlem  28885  pthdlem1  28888  pthd  28891  crctcshwlkn0  28940  2wlkdlem4  29047  2wlkdlem5  29048  2pthdlem1  29049  2wlkdlem10  29054  rusgrnumwwlkl1  29087  0ewlk  29232  0wlk  29234  wlk2v2elem2  29274  3wlkdlem4  29280  3wlkdlem5  29281  3pthdlem1  29282  3wlkdlem10  29287  minvecolem1  29990  minvecolem5  29997  minvecolem6  29998  cdj3lem3b  31556  prsiga  32960  hfext  34985  filnetlem4  35070  relowlssretop  36048  relowlpssretop  36049  elghomOLD  36560  iscrngo2  36670  refrelcoss3  37138  tendoset  39435  fnwe2lem2  41564  nadd1suc  41913  eliuniincex  43569  eliincex  43570  uzub  43914  liminflelimsuplem  44264  xlimbr  44316  subsaliuncl  44847  isomushgr  46266  rrx2pnecoorneor  47049  rrx2linest  47076