Theorem raleqdv 2671

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 2665	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 14	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453

This theorem is referenced by:  raleqbidv  2677  raleqbidva  2679  omsinds  4604  cbvfo  5761  isoselem  5796  ofrfval  6066  issmo2  6265  smoeq  6266  tfrlemisucaccv  6301  tfr1onlemsucaccv  6317  tfrcllemsucaccv  6330  nninfisollem0  7102  fzrevral2  10049  fzrevral3  10050  fzshftral  10051  fzoshftral  10181  uzsinds  10385  iseqf1olemqk  10437  seq3f1olemstep  10444  seq3f1olemp  10445  caucvgre  10932  cvg1nlemres  10936  rexuz3  10941  resqrexlemoverl  10972  resqrexlemsqa  10975  resqrexlemex  10976  climconst  11240  climshftlemg  11252  serf0  11302  summodclem2  11332  summodc  11333  zsumdc  11334  mertenslemi1  11485  prodmodclem2  11527  prodmodc  11528  zproddc  11529  zsupcllemstep  11887  zsupcllemex  11888  infssuzex  11891  suprzubdc  11894  nninfdcex  11895  prmind2  12061  ennnfoneleminc  12353  ennnfonelemex  12356  ennnfonelemnn0  12364  ennnfonelemr  12365  grpidpropdg  12615  mndpropd  12663  lmfval  12945  lmconst  12969  cncnp  12983  metss  13247  sin0pilem2  13456  2sqlem10  13714  nninfsellemdc  14003  nninfself  14006  nninfsellemeqinf  14009  nninfomni  14012