Theorem raleqi 3295

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

Syntax hints:   ↔ wb 207   = wceq 1547  ∀wral 3053

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 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ral 3054  df-rex 3064

This theorem is referenced by:  ralrab2  3639  ralprgf  4626  ralprg  4628  raltpg  4630  ralxp  5783  f12dfv  7217  f13dfv  7218  ralrnmpo  7495  ovmptss  8032  ixpfi2  9250  dffi3  9334  dfoi  9416  ssttrcl  9627  fseqenlem1  9937  kmlem12  10075  fzprval  13530  fztpval  13531  hashbc  14406  2prm  16652  prmreclem2  16879  xpsfrnel  17517  xpsle  17534  s1chn  18577  chnub  18579  gsumwspan  18805  sgrp2rid2  18888  psgnunilem3  19462  pmtrsn  19485  islinds2  21788  ply1coe  22284  cply1coe0bi  22288  m2cpminvid2lem  22737  basdif0  22936  ordtbaslem  23171  ptbasfi  23564  ptcnplem  23604  ptrescn  23622  flftg  23979  ust0  24203  minveclem1  25409  minveclem3b  25413  minveclem6  25419  iblcnlem1  25773  ellimc2  25862  ftalem3  27056  dchreq  27239  pntlem3  27590  negbdaylem  28066  precsexlem9  28225  0reno  28506  1reno  28507  istrkg2ld  28546  istrkg3ld  28547  tgcgr4  28617  elntg2  29072  lfuhgr1v0e  29341  cplgr0  29512  wlkp1lem8  29765  usgr2pthlem  29849  pthdlem1  29852  pthd  29855  crctcshwlkn0  29907  2wlkdlem4  30014  2wlkdlem5  30015  2pthdlem1  30016  2wlkdlem10  30021  rusgrnumwwlkl1  30057  0ewlk  30202  0wlk  30204  wlk2v2elem2  30244  3wlkdlem4  30250  3wlkdlem5  30251  3pthdlem1  30252  3wlkdlem10  30257  minvecolem1  30963  minvecolem5  30970  minvecolem6  30971  cdj3lem3b  32529  elrgspnsubrunlem2  33329  prsiga  34315  hfext  36411  filnetlem4  36609  mh-infprim2bi  36775  relowlssretop  37725  relowlpssretop  37726  elghomOLD  38254  iscrngo2  38364  refrelcoss3  38920  tendoset  41251  fnwe2lem2  43496  nadd1suc  43837  eliuniincex  45556  eliincex  45557  uzub  45874  liminflelimsuplem  46218  xlimbr  46270  subsaliuncl  46801  gricushgr  48408  isgrlim  48473  rrx2pnecoorneor  49206  rrx2linest  49233