Theorem raleqdv 2679

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 2673	. 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  2685  raleqbidva  2687  omsinds  4622  cbvfo  5786  isoselem  5821  ofrfval  6091  issmo2  6290  smoeq  6291  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  nninfisollem0  7128  fzrevral2  10106  fzrevral3  10107  fzshftral  10108  fzoshftral  10238  uzsinds  10442  iseqf1olemqk  10494  seq3f1olemstep  10501  seq3f1olemp  10502  caucvgre  10990  cvg1nlemres  10994  rexuz3  10999  resqrexlemoverl  11030  resqrexlemsqa  11033  resqrexlemex  11034  climconst  11298  climshftlemg  11310  serf0  11360  summodclem2  11390  summodc  11391  zsumdc  11392  mertenslemi1  11543  prodmodclem2  11585  prodmodc  11586  zproddc  11587  zsupcllemstep  11946  zsupcllemex  11947  infssuzex  11950  suprzubdc  11953  nninfdcex  11954  prmind2  12120  ennnfoneleminc  12412  ennnfonelemex  12415  ennnfonelemnn0  12423  ennnfonelemr  12424  grpidpropdg  12793  mndpropd  12841  nmznsg  13073  cmnpropd  13098  ringpropd  13217  lmfval  13695  lmconst  13719  cncnp  13733  metss  13997  sin0pilem2  14206  2sqlem10  14475  nninfsellemdc  14762  nninfself  14765  nninfsellemeqinf  14768  nninfomni  14771