Theorem raleqi 3294

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

Syntax hints:   ↔ wb 206   = wceq 1541  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ral 3052  df-rex 3061

This theorem is referenced by:  ralrab2  3656  ralprgf  4651  ralprg  4653  raltpg  4655  ralxp  5790  f12dfv  7219  f13dfv  7220  ralrnmpo  7497  ovmptss  8035  ixpfi2  9250  dffi3  9334  dfoi  9416  ssttrcl  9624  fseqenlem1  9934  kmlem12  10072  fzprval  13501  fztpval  13502  hashbc  14376  2prm  16619  prmreclem2  16845  xpsfrnel  17483  xpsle  17500  s1chn  18543  chnub  18545  gsumwspan  18771  sgrp2rid2  18851  psgnunilem3  19425  pmtrsn  19448  islinds2  21768  ply1coe  22242  cply1coe0bi  22246  m2cpminvid2lem  22698  basdif0  22897  ordtbaslem  23132  ptbasfi  23525  ptcnplem  23565  ptrescn  23583  flftg  23940  ust0  24164  minveclem1  25380  minveclem3b  25384  minveclem6  25390  iblcnlem1  25745  ellimc2  25834  ftalem3  27041  dchreq  27225  pntlem3  27576  negbdaylem  28052  precsexlem9  28211  0reno  28492  1reno  28493  istrkg2ld  28532  istrkg3ld  28533  tgcgr4  28603  elntg2  29058  lfuhgr1v0e  29327  cplgr0  29498  wlkp1lem8  29752  usgr2pthlem  29836  pthdlem1  29839  pthd  29842  crctcshwlkn0  29894  2wlkdlem4  30001  2wlkdlem5  30002  2pthdlem1  30003  2wlkdlem10  30008  rusgrnumwwlkl1  30044  0ewlk  30189  0wlk  30191  wlk2v2elem2  30231  3wlkdlem4  30237  3wlkdlem5  30238  3pthdlem1  30239  3wlkdlem10  30244  minvecolem1  30949  minvecolem5  30956  minvecolem6  30957  cdj3lem3b  32515  elrgspnsubrunlem2  33330  prsiga  34288  hfext  36377  filnetlem4  36575  relowlssretop  37568  relowlpssretop  37569  elghomOLD  38088  iscrngo2  38198  refrelcoss3  38736  tendoset  41029  fnwe2lem2  43303  nadd1suc  43644  eliuniincex  45363  eliincex  45364  uzub  45685  liminflelimsuplem  46029  xlimbr  46081  subsaliuncl  46612  gricushgr  48173  isgrlim  48238  rrx2pnecoorneor  48971  rrx2linest  48998