Theorem raleqi 3312

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

Syntax hints:   ↔ wb 205   = wceq 1533  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ral 3051  df-rex 3060

This theorem is referenced by:  ralrab2  3690  ralprgf  4698  ralprg  4700  raltpg  4704  ralxp  5844  f12dfv  7282  f13dfv  7283  ralrnmpo  7560  ovmptss  8098  ixpfi2  9376  dffi3  9456  dfoi  9536  ssttrcl  9740  fseqenlem1  10049  kmlem12  10186  fzprval  13597  fztpval  13598  hashbc  14448  2prm  16666  prmreclem2  16889  xpsfrnel  17547  xpsle  17564  gsumwspan  18806  sgrp2rid2  18886  psgnunilem3  19463  pmtrsn  19486  islinds2  21764  ply1coe  22242  cply1coe0bi  22246  m2cpminvid2lem  22700  basdif0  22900  ordtbaslem  23136  ptbasfi  23529  ptcnplem  23569  ptrescn  23587  flftg  23944  ust0  24168  minveclem1  25396  minveclem3b  25400  minveclem6  25406  iblcnlem1  25761  ellimc2  25850  ftalem3  27052  dchreq  27236  pntlem3  27587  negsbdaylem  28014  precsexlem9  28163  istrkg2ld  28336  istrkg3ld  28337  tgcgr4  28407  elntg2  28868  lfuhgr1v0e  29139  cplgr0  29310  wlkp1lem8  29566  usgr2pthlem  29649  pthdlem1  29652  pthd  29655  crctcshwlkn0  29704  2wlkdlem4  29811  2wlkdlem5  29812  2pthdlem1  29813  2wlkdlem10  29818  rusgrnumwwlkl1  29851  0ewlk  29996  0wlk  29998  wlk2v2elem2  30038  3wlkdlem4  30044  3wlkdlem5  30045  3pthdlem1  30046  3wlkdlem10  30051  minvecolem1  30756  minvecolem5  30763  minvecolem6  30764  cdj3lem3b  32322  prsiga  33881  hfext  35910  filnetlem4  35996  relowlssretop  36973  relowlpssretop  36974  elghomOLD  37491  iscrngo2  37601  refrelcoss3  38065  tendoset  40362  fnwe2lem2  42617  nadd1suc  42963  eliuniincex  44615  eliincex  44616  uzub  44951  liminflelimsuplem  45301  xlimbr  45353  subsaliuncl  45884  gricushgr  47369  rrx2pnecoorneor  47974  rrx2linest  48001