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  4655  cbvfo  5829  isoselem  5864  ofrfval  6141  issmo2  6344  smoeq  6345  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  nninfisollem0  7191  fzrevral2  10175  fzrevral3  10176  fzshftral  10177  fzoshftral  10308  uzsinds  10518  iseqf1olemqk  10581  seq3f1olemstep  10588  seq3f1olemp  10589  caucvgre  11128  cvg1nlemres  11132  rexuz3  11137  resqrexlemoverl  11168  resqrexlemsqa  11171  resqrexlemex  11172  climconst  11436  climshftlemg  11448  serf0  11498  summodclem2  11528  summodc  11529  zsumdc  11530  mertenslemi1  11681  prodmodclem2  11723  prodmodc  11724  zproddc  11725  zsupcllemstep  12085  zsupcllemex  12086  infssuzex  12089  suprzubdc  12092  nninfdcex  12093  prmind2  12261  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemnn0  12582  ennnfonelemr  12583  grpidpropdg  12960  sgrppropd  12999  mndpropd  13024  nmznsg  13286  ghmnsgima  13341  cmnpropd  13368  rngpropd  13454  ringpropd  13537  lsspropdg  13930  isridlrng  13981  lmfval  14371  lmconst  14395  cncnp  14409  metss  14673  sin0pilem2  14958  2sqlem10  15282  nninfsellemdc  15570  nninfself  15573  nninfsellemeqinf  15576  nninfomni  15579