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  4606  cbvfo  5764  isoselem  5799  ofrfval  6069  issmo2  6268  smoeq  6269  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  nninfisollem0  7106  fzrevral2  10062  fzrevral3  10063  fzshftral  10064  fzoshftral  10194  uzsinds  10398  iseqf1olemqk  10450  seq3f1olemstep  10457  seq3f1olemp  10458  caucvgre  10945  cvg1nlemres  10949  rexuz3  10954  resqrexlemoverl  10985  resqrexlemsqa  10988  resqrexlemex  10989  climconst  11253  climshftlemg  11265  serf0  11315  summodclem2  11345  summodc  11346  zsumdc  11347  mertenslemi1  11498  prodmodclem2  11540  prodmodc  11541  zproddc  11542  zsupcllemstep  11900  zsupcllemex  11901  infssuzex  11904  suprzubdc  11907  nninfdcex  11908  prmind2  12074  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemnn0  12377  ennnfonelemr  12378  grpidpropdg  12628  mndpropd  12676  lmfval  12986  lmconst  13010  cncnp  13024  metss  13288  sin0pilem2  13497  2sqlem10  13755  nninfsellemdc  14043  nninfself  14046  nninfsellemeqinf  14049  nninfomni  14052