Theorem raleqi 3142

Description: Equality inference for restricted universal qualifier. (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 3138	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

Syntax hints:   ↔ wb 196   = wceq 1483  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917

This theorem is referenced by:  ralrab2  3372  ralprg  4234  raltpg  4236  ralxp  5263  f12dfv  6529  f13dfv  6530  ralrnmpt2  6775  ovmptss  7258  ixpfi2  8264  dffi3  8337  dfoi  8416  fseqenlem1  8847  kmlem12  8983  fzprval  12401  fztpval  12402  hashbc  13237  2prm  15405  prmreclem2  15621  xpsfrnel  16223  xpsle  16241  gsumwspan  17383  sgrp2rid2  17413  psgnunilem3  17916  pmtrsn  17939  ply1coe  19666  cply1coe0bi  19670  islinds2  20152  m2cpminvid2lem  20559  basdif0  20757  ordtbaslem  20992  ptbasfi  21384  ptcnplem  21424  ptrescn  21442  flftg  21800  ust0  22023  minveclem1  23195  minveclem3b  23199  minveclem6  23205  iblcnlem1  23554  ellimc2  23641  ftalem3  24801  dchreq  24983  pntlem3  25298  istrkg2ld  25359  istrkg3ld  25360  lfuhgr1v0e  26146  cplgr0  26321  wlkp1lem8  26577  usgr2pthlem  26659  pthdlem1  26662  pthd  26665  crctcshwlkn0  26713  2wlkdlem4  26824  2wlkdlem5  26825  2pthdlem1  26826  2wlkdlem10  26831  rusgrnumwwlkl1  26863  0ewlk  26975  0wlk  26977  wlk2v2elem2  27016  3wlkdlem4  27022  3wlkdlem5  27023  3pthdlem1  27024  3wlkdlem10  27029  minvecolem1  27730  minvecolem5  27737  minvecolem6  27738  cdj3lem3b  29299  prsiga  30194  hfext  32290  filnetlem4  32376  relowlssretop  33211  relowlpssretop  33212  elghomOLD  33686  iscrngo2  33796  tendoset  36047  fnwe2lem2  37621  eliuniincex  39292  eliincex  39293  uzub  39658  liminflelimsuplem  40007  xlimbr  40053  subsaliuncl  40576