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  9252  dffi3  9336  dfoi  9418  ssttrcl  9626  fseqenlem1  9936  kmlem12  10074  fzprval  13503  fztpval  13504  hashbc  14378  2prm  16621  prmreclem2  16847  xpsfrnel  17485  xpsle  17502  s1chn  18545  chnub  18547  gsumwspan  18773  sgrp2rid2  18853  psgnunilem3  19427  pmtrsn  19450  islinds2  21770  ply1coe  22244  cply1coe0bi  22248  m2cpminvid2lem  22700  basdif0  22899  ordtbaslem  23134  ptbasfi  23527  ptcnplem  23567  ptrescn  23585  flftg  23942  ust0  24166  minveclem1  25382  minveclem3b  25386  minveclem6  25392  iblcnlem1  25747  ellimc2  25836  ftalem3  27043  dchreq  27227  pntlem3  27578  negbdaylem  28054  precsexlem9  28213  0reno  28494  1reno  28495  istrkg2ld  28534  istrkg3ld  28535  tgcgr4  28605  elntg2  29060  lfuhgr1v0e  29329  cplgr0  29500  wlkp1lem8  29754  usgr2pthlem  29838  pthdlem1  29841  pthd  29844  crctcshwlkn0  29896  2wlkdlem4  30003  2wlkdlem5  30004  2pthdlem1  30005  2wlkdlem10  30010  rusgrnumwwlkl1  30046  0ewlk  30191  0wlk  30193  wlk2v2elem2  30233  3wlkdlem4  30239  3wlkdlem5  30240  3pthdlem1  30241  3wlkdlem10  30246  minvecolem1  30951  minvecolem5  30958  minvecolem6  30959  cdj3lem3b  32517  elrgspnsubrunlem2  33332  prsiga  34290  hfext  36379  filnetlem4  36577  relowlssretop  37570  relowlpssretop  37571  elghomOLD  38090  iscrngo2  38200  refrelcoss3  38748  tendoset  41041  fnwe2lem2  43314  nadd1suc  43655  eliuniincex  45374  eliincex  45375  uzub  45696  liminflelimsuplem  46040  xlimbr  46092  subsaliuncl  46623  gricushgr  48184  isgrlim  48249  rrx2pnecoorneor  48982  rrx2linest  49009