Theorem raleqdv 2708

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  ∀wral 2484

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489

This theorem is referenced by:  raleqtrdv  2710  raleqtrrdv  2712  raleqbidv  2718  raleqbidva  2720  omsinds  4670  cbvfo  5854  isoselem  5889  ofrfval  6167  issmo2  6375  smoeq  6376  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  nninfisollem0  7232  isacnm  7315  fzrevral2  10228  fzrevral3  10229  fzshftral  10230  fzoshftral  10367  zsupcllemstep  10372  zsupcllemex  10373  infssuzex  10376  suprzubdc  10379  nninfdcex  10380  uzsinds  10589  iseqf1olemqk  10652  seq3f1olemstep  10659  seq3f1olemp  10660  eqs1  11082  swrdspsleq  11120  caucvgre  11292  cvg1nlemres  11296  rexuz3  11301  resqrexlemoverl  11332  resqrexlemsqa  11335  resqrexlemex  11336  climconst  11601  climshftlemg  11613  serf0  11663  summodclem2  11693  summodc  11694  zsumdc  11695  mertenslemi1  11846  prodmodclem2  11888  prodmodc  11889  zproddc  11890  prmind2  12442  ennnfoneleminc  12782  ennnfonelemex  12785  ennnfonelemnn0  12793  ennnfonelemr  12794  grpidpropdg  13206  sgrppropd  13245  mndpropd  13272  nmznsg  13549  ghmnsgima  13604  cmnpropd  13631  rngpropd  13717  ringpropd  13800  lsspropdg  14193  isridlrng  14244  mplvalcoe  14452  lmfval  14664  lmconst  14688  cncnp  14702  metss  14966  sin0pilem2  15254  fsumdvdsmul  15463  2sqlem10  15602  nninfsellemdc  15947  nninfself  15950  nninfsellemeqinf  15953  nninfomni  15956