Theorem raleqi 3332

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

Syntax hints:   ↔ wb 206   = wceq 1537  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ral 3068  df-rex 3077

This theorem is referenced by:  ralrab2  3720  ralprgf  4717  ralprg  4719  raltpg  4723  ralxp  5866  f12dfv  7309  f13dfv  7310  ralrnmpo  7589  ovmptss  8134  ixpfi2  9420  dffi3  9500  dfoi  9580  ssttrcl  9784  fseqenlem1  10093  kmlem12  10231  fzprval  13645  fztpval  13646  hashbc  14502  2prm  16739  prmreclem2  16964  xpsfrnel  17622  xpsle  17639  gsumwspan  18881  sgrp2rid2  18961  psgnunilem3  19538  pmtrsn  19561  islinds2  21856  ply1coe  22323  cply1coe0bi  22327  m2cpminvid2lem  22781  basdif0  22981  ordtbaslem  23217  ptbasfi  23610  ptcnplem  23650  ptrescn  23668  flftg  24025  ust0  24249  minveclem1  25477  minveclem3b  25481  minveclem6  25487  iblcnlem1  25843  ellimc2  25932  ftalem3  27136  dchreq  27320  pntlem3  27671  negsbdaylem  28106  precsexlem9  28257  istrkg2ld  28486  istrkg3ld  28487  tgcgr4  28557  elntg2  29018  lfuhgr1v0e  29289  cplgr0  29460  wlkp1lem8  29716  usgr2pthlem  29799  pthdlem1  29802  pthd  29805  crctcshwlkn0  29854  2wlkdlem4  29961  2wlkdlem5  29962  2pthdlem1  29963  2wlkdlem10  29968  rusgrnumwwlkl1  30001  0ewlk  30146  0wlk  30148  wlk2v2elem2  30188  3wlkdlem4  30194  3wlkdlem5  30195  3pthdlem1  30196  3wlkdlem10  30201  minvecolem1  30906  minvecolem5  30913  minvecolem6  30914  cdj3lem3b  32472  chnub  32984  prsiga  34095  hfext  36147  filnetlem4  36347  relowlssretop  37329  relowlpssretop  37330  elghomOLD  37847  iscrngo2  37957  refrelcoss3  38419  tendoset  40716  fnwe2lem2  43008  nadd1suc  43354  eliuniincex  45011  eliincex  45012  uzub  45346  liminflelimsuplem  45696  xlimbr  45748  subsaliuncl  46279  gricushgr  47770  isgrlim  47806  rrx2pnecoorneor  48449  rrx2linest  48476