Theorem raleqi 3320

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ral 3080  df-rex 3090

This theorem is used by:  ralrab2  3658  ralprgf  4654  ralprg  4656  raltpg  4658  ralxp  5822  f12dfv  7288  f13dfv  7289  ralrnmpo  7566  ovmptssOLD  8113  fnwe2lem3  8157  ixpfi2  9350  dffi3  9433  dfoi  9515  ssttrcl  9726  fseqenlem1  10113  kmlem12  10250  fzprval  13729  fztpval  13730  hashbc  14608  2prm  16879  prmreclem2  17107  xpsfrnel  17746  xpsle  17763  s1chn  18806  chnub  18808  gsumwspan  19054  sgrp2rid2  19137  psgnunilem3  19722  pmtrsn  19745  islinds2  22131  ply1coe  22628  cply1coe0bi  22632  m2cpminvid2lem  23084  basdif0  23283  ordtbaslem  23518  ptbasfi  23912  ptcnplem  23952  ptrescn  23970  flftg  24327  ust0  24551  minveclem1  25757  minveclem3b  25761  minveclem6  25767  iblcnlem1  26120  ellimc2  26209  ftalem3  27414  dchreq  27597  pntlem3  27948  negbdaylem  28454  precsexlem9  28613  0reno  28894  1reno  28895  istrkg2ld  28934  istrkg3ld  28935  tgcgr4  29006  elntg2  29575  lfuhgr1v0e  29847  cplgr0  30018  wlkp1lem8  30271  usgr2pthlem  30361  pthdlem1  30364  pthd  30367  crctcshwlkn0  30422  2wlkdlem4  30529  2wlkdlem5  30530  2pthdlem1  30531  2wlkdlem10  30536  rusgrnumwwlkl1  30572  0ewlk  30717  0wlk  30719  wlk2v2elem2  30769  3wlkdlem4  30775  3wlkdlem5  30776  3pthdlem1  30777  3wlkdlem10  30782  minvecolem1  31488  minvecolem5  31495  minvecolem6  31496  cdj3lem3b  33054  elrgspnsubrunlem2  33862  prsiga  34816  hfext  37061  nmulrid  37073  filnetlem4  37296  mh-infprim2bi  37462  relowlssretop  38426  relowlpssretop  38427  elghomOLD  38961  iscrngo2  39071  refrelcoss3  39625  tendoset  41956  nadd1suc  44534  eliuniincex  46263  eliincex  46264  uzub  46580  liminflelimsuplem  46924  xlimbr  46976  subsaliuncl  47507  gricushgr  49154  isgrlim  49219  rrx2pnecoorneor  49967  rrx2linest  49993