Theorem raleqdv 2678

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  ∀wral 2455

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  raleqbidv  2684  raleqbidva  2686  omsinds  4621  cbvfo  5785  isoselem  5820  ofrfval  6090  issmo2  6289  smoeq  6290  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  nninfisollem0  7127  fzrevral2  10105  fzrevral3  10106  fzshftral  10107  fzoshftral  10237  uzsinds  10441  iseqf1olemqk  10493  seq3f1olemstep  10500  seq3f1olemp  10501  caucvgre  10989  cvg1nlemres  10993  rexuz3  10998  resqrexlemoverl  11029  resqrexlemsqa  11032  resqrexlemex  11033  climconst  11297  climshftlemg  11309  serf0  11359  summodclem2  11389  summodc  11390  zsumdc  11391  mertenslemi1  11542  prodmodclem2  11584  prodmodc  11585  zproddc  11586  zsupcllemstep  11945  zsupcllemex  11946  infssuzex  11949  suprzubdc  11952  nninfdcex  11953  prmind2  12119  ennnfoneleminc  12411  ennnfonelemex  12414  ennnfonelemnn0  12422  ennnfonelemr  12423  grpidpropdg  12792  mndpropd  12840  nmznsg  13071  cmnpropd  13096  ringpropd  13215  lmfval  13662  lmconst  13686  cncnp  13700  metss  13964  sin0pilem2  14173  2sqlem10  14442  nninfsellemdc  14729  nninfself  14732  nninfsellemeqinf  14735  nninfomni  14738