Theorem raleqi 3322

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ral 3060  df-rex 3069

This theorem is referenced by:  ralrab2  3707  ralprgf  4699  ralprg  4701  raltpg  4703  ralxp  5855  f12dfv  7293  f13dfv  7294  ralrnmpo  7572  ovmptss  8117  ixpfi2  9388  dffi3  9469  dfoi  9549  ssttrcl  9753  fseqenlem1  10062  kmlem12  10200  fzprval  13622  fztpval  13623  hashbc  14489  2prm  16726  prmreclem2  16951  xpsfrnel  17609  xpsle  17626  gsumwspan  18872  sgrp2rid2  18952  psgnunilem3  19529  pmtrsn  19552  islinds2  21851  ply1coe  22318  cply1coe0bi  22322  m2cpminvid2lem  22776  basdif0  22976  ordtbaslem  23212  ptbasfi  23605  ptcnplem  23645  ptrescn  23663  flftg  24020  ust0  24244  minveclem1  25472  minveclem3b  25476  minveclem6  25482  iblcnlem1  25838  ellimc2  25927  ftalem3  27133  dchreq  27317  pntlem3  27668  negsbdaylem  28103  precsexlem9  28254  istrkg2ld  28483  istrkg3ld  28484  tgcgr4  28554  elntg2  29015  lfuhgr1v0e  29286  cplgr0  29457  wlkp1lem8  29713  usgr2pthlem  29796  pthdlem1  29799  pthd  29802  crctcshwlkn0  29851  2wlkdlem4  29958  2wlkdlem5  29959  2pthdlem1  29960  2wlkdlem10  29965  rusgrnumwwlkl1  29998  0ewlk  30143  0wlk  30145  wlk2v2elem2  30185  3wlkdlem4  30191  3wlkdlem5  30192  3pthdlem1  30193  3wlkdlem10  30198  minvecolem1  30903  minvecolem5  30910  minvecolem6  30911  cdj3lem3b  32469  chnub  32986  prsiga  34112  hfext  36165  filnetlem4  36364  relowlssretop  37346  relowlpssretop  37347  elghomOLD  37874  iscrngo2  37984  refrelcoss3  38445  tendoset  40742  fnwe2lem2  43040  nadd1suc  43382  eliuniincex  45049  eliincex  45050  uzub  45381  liminflelimsuplem  45731  xlimbr  45783  subsaliuncl  46314  gricushgr  47824  isgrlim  47885  rrx2pnecoorneor  48565  rrx2linest  48592