Theorem raleqi 3323

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

Syntax hints:   ↔ wb 206   = wceq 1539  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

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

This theorem is referenced by:  ralrab2  3703  ralprgf  4693  ralprg  4695  raltpg  4697  ralxp  5851  f12dfv  7294  f13dfv  7295  ralrnmpo  7573  ovmptss  8119  ixpfi2  9391  dffi3  9472  dfoi  9552  ssttrcl  9756  fseqenlem1  10065  kmlem12  10203  fzprval  13626  fztpval  13627  hashbc  14493  2prm  16730  prmreclem2  16956  xpsfrnel  17608  xpsle  17625  gsumwspan  18860  sgrp2rid2  18940  psgnunilem3  19515  pmtrsn  19538  islinds2  21834  ply1coe  22303  cply1coe0bi  22307  m2cpminvid2lem  22761  basdif0  22961  ordtbaslem  23197  ptbasfi  23590  ptcnplem  23630  ptrescn  23648  flftg  24005  ust0  24229  minveclem1  25459  minveclem3b  25463  minveclem6  25469  iblcnlem1  25824  ellimc2  25913  ftalem3  27119  dchreq  27303  pntlem3  27654  negsbdaylem  28089  precsexlem9  28240  istrkg2ld  28469  istrkg3ld  28470  tgcgr4  28540  elntg2  29001  lfuhgr1v0e  29272  cplgr0  29443  wlkp1lem8  29699  usgr2pthlem  29784  pthdlem1  29787  pthd  29790  crctcshwlkn0  29842  2wlkdlem4  29949  2wlkdlem5  29950  2pthdlem1  29951  2wlkdlem10  29956  rusgrnumwwlkl1  29989  0ewlk  30134  0wlk  30136  wlk2v2elem2  30176  3wlkdlem4  30182  3wlkdlem5  30183  3pthdlem1  30184  3wlkdlem10  30189  minvecolem1  30894  minvecolem5  30901  minvecolem6  30902  cdj3lem3b  32460  s1chn  33001  chnub  33003  elrgspnsubrunlem2  33253  prsiga  34133  hfext  36185  filnetlem4  36383  relowlssretop  37365  relowlpssretop  37366  elghomOLD  37895  iscrngo2  38005  refrelcoss3  38465  tendoset  40762  fnwe2lem2  43068  nadd1suc  43410  eliuniincex  45119  eliincex  45120  uzub  45447  liminflelimsuplem  45795  xlimbr  45847  subsaliuncl  46378  gricushgr  47891  isgrlim  47954  rrx2pnecoorneor  48641  rrx2linest  48668