Theorem raleqdv 2711

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491

This theorem is referenced by:  raleqtrdv  2713  raleqtrrdv  2715  raleqbidv  2721  raleqbidva  2723  omsinds  4688  cbvfo  5877  isoselem  5912  ofrfval  6190  issmo2  6398  smoeq  6399  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  nninfisollem0  7258  isacnm  7346  fzrevral2  10263  fzrevral3  10264  fzshftral  10265  fzoshftral  10404  zsupcllemstep  10409  zsupcllemex  10410  infssuzex  10413  suprzubdc  10416  nninfdcex  10417  uzsinds  10626  iseqf1olemqk  10689  seq3f1olemstep  10696  seq3f1olemp  10697  eqs1  11120  swrdspsleq  11158  pfxeq  11187  pfxsuffeqwrdeq  11189  caucvgre  11407  cvg1nlemres  11411  rexuz3  11416  resqrexlemoverl  11447  resqrexlemsqa  11450  resqrexlemex  11451  climconst  11716  climshftlemg  11728  serf0  11778  summodclem2  11808  summodc  11809  zsumdc  11810  mertenslemi1  11961  prodmodclem2  12003  prodmodc  12004  zproddc  12005  prmind2  12557  ennnfoneleminc  12897  ennnfonelemex  12900  ennnfonelemnn0  12908  ennnfonelemr  12909  grpidpropdg  13321  sgrppropd  13360  mndpropd  13387  nmznsg  13664  ghmnsgima  13719  cmnpropd  13746  rngpropd  13832  ringpropd  13915  lsspropdg  14308  isridlrng  14359  mplvalcoe  14567  lmfval  14779  lmconst  14803  cncnp  14817  metss  15081  sin0pilem2  15369  fsumdvdsmul  15578  2sqlem10  15717  nninfsellemdc  16149  nninfself  16152  nninfsellemeqinf  16155  nninfomni  16158