Theorem raleqdv 2696

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364  ∀wral 2472

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477

This theorem is referenced by:  raleqtrdv  2698  raleqtrrdv  2700  raleqbidv  2706  raleqbidva  2708  omsinds  4654  cbvfo  5828  isoselem  5863  ofrfval  6139  issmo2  6342  smoeq  6343  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  nninfisollem0  7189  fzrevral2  10172  fzrevral3  10173  fzshftral  10174  fzoshftral  10305  uzsinds  10515  iseqf1olemqk  10578  seq3f1olemstep  10585  seq3f1olemp  10586  caucvgre  11125  cvg1nlemres  11129  rexuz3  11134  resqrexlemoverl  11165  resqrexlemsqa  11168  resqrexlemex  11169  climconst  11433  climshftlemg  11445  serf0  11495  summodclem2  11525  summodc  11526  zsumdc  11527  mertenslemi1  11678  prodmodclem2  11720  prodmodc  11721  zproddc  11722  zsupcllemstep  12082  zsupcllemex  12083  infssuzex  12086  suprzubdc  12089  nninfdcex  12090  prmind2  12258  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemnn0  12579  ennnfonelemr  12580  grpidpropdg  12957  sgrppropd  12996  mndpropd  13021  nmznsg  13283  ghmnsgima  13338  cmnpropd  13365  rngpropd  13451  ringpropd  13534  lsspropdg  13927  isridlrng  13978  lmfval  14360  lmconst  14384  cncnp  14398  metss  14662  sin0pilem2  14917  2sqlem10  15212  nninfsellemdc  15500  nninfself  15503  nninfsellemeqinf  15506  nninfomni  15509