Theorem raleqdv 2736

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)

Hypothesis

Ref	Expression
raleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
raleqdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		raleq 2730	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 14	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  raleqtrdv  2738  raleqtrrdv  2740  raleqbidv  2746  raleqbidva  2748  omsinds  4720  cbvfo  5926  isoselem  5961  ofrfval  6244  issmo2  6455  smoeq  6456  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  nninfisollem0  7329  isacnm  7418  fzrevral2  10341  fzrevral3  10342  fzshftral  10343  fzoshftral  10485  zsupcllemstep  10490  zsupcllemex  10491  infssuzex  10494  suprzubdc  10497  nninfdcex  10498  uzsinds  10707  iseqf1olemqk  10770  seq3f1olemstep  10777  seq3f1olemp  10778  eqs1  11209  swrdspsleq  11252  pfxeq  11281  pfxsuffeqwrdeq  11283  caucvgre  11559  cvg1nlemres  11563  rexuz3  11568  resqrexlemoverl  11599  resqrexlemsqa  11602  resqrexlemex  11603  climconst  11868  climshftlemg  11880  serf0  11930  summodclem2  11961  summodc  11962  zsumdc  11963  mertenslemi1  12114  prodmodclem2  12156  prodmodc  12157  zproddc  12158  prmind2  12710  ennnfoneleminc  13050  ennnfonelemex  13053  ennnfonelemnn0  13061  ennnfonelemr  13062  grpidpropdg  13475  sgrppropd  13514  mndpropd  13541  nmznsg  13818  ghmnsgima  13873  cmnpropd  13900  rngpropd  13987  ringpropd  14070  lsspropdg  14464  isridlrng  14515  mplvalcoe  14723  lmfval  14936  lmconst  14959  cncnp  14973  metss  15237  sin0pilem2  15525  fsumdvdsmul  15734  2sqlem10  15873  usgruspgrben  16056  wlkeq  16224  wlkl1loop  16228  uspgr2wlkeq  16235  upgr2wlkdc  16247  clwwlkccatlem  16270  clwwlknp  16287  clwwlkn1  16288  clwwlkn2  16291  nninfsellemdc  16663  nninfself  16666  nninfsellemeqinf  16669  nninfomni  16672