Theorem raleqi 3345

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

Syntax hints:   ↔ wb 205   = wceq 1542  ∀wral 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732  df-ral 3071

This theorem is referenced by:  ralrab2  3638  ralprgf  4634  ralprg  4636  raltpg  4640  ralxp  5749  f12dfv  7142  f13dfv  7143  ralrnmpo  7407  ovmptss  7925  ixpfi2  9105  dffi3  9178  dfoi  9258  ssttrcl  9461  fseqenlem1  9791  kmlem12  9928  fzprval  13328  fztpval  13329  hashbc  14176  2prm  16408  prmreclem2  16629  xpsfrnel  17284  xpsle  17301  gsumwspan  18496  sgrp2rid2  18576  psgnunilem3  19115  pmtrsn  19138  islinds2  21031  ply1coe  21478  cply1coe0bi  21482  m2cpminvid2lem  21914  basdif0  22114  ordtbaslem  22350  ptbasfi  22743  ptcnplem  22783  ptrescn  22801  flftg  23158  ust0  23382  minveclem1  24599  minveclem3b  24603  minveclem6  24609  iblcnlem1  24963  ellimc2  25052  ftalem3  26235  dchreq  26417  pntlem3  26768  istrkg2ld  26832  istrkg3ld  26833  tgcgr4  26903  elntg2  27364  lfuhgr1v0e  27632  cplgr0  27803  wlkp1lem8  28058  usgr2pthlem  28140  pthdlem1  28143  pthd  28146  crctcshwlkn0  28195  2wlkdlem4  28302  2wlkdlem5  28303  2pthdlem1  28304  2wlkdlem10  28309  rusgrnumwwlkl1  28342  0ewlk  28487  0wlk  28489  wlk2v2elem2  28529  3wlkdlem4  28535  3wlkdlem5  28536  3pthdlem1  28537  3wlkdlem10  28542  minvecolem1  29245  minvecolem5  29252  minvecolem6  29253  cdj3lem3b  30811  prsiga  32108  hfext  34494  filnetlem4  34579  relowlssretop  35543  relowlpssretop  35544  elghomOLD  36054  iscrngo2  36164  refrelcoss3  36590  tendoset  38782  fnwe2lem2  40885  eliuniincex  42641  eliincex  42642  uzub  42953  liminflelimsuplem  43298  xlimbr  43350  subsaliuncl  43879  isomushgr  45257  rrx2pnecoorneor  46040  rrx2linest  46067