Theorem raleqdv 2749

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  ∀wral 2522

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527

This theorem is referenced by:  raleqtrdv  2751  raleqtrrdv  2753  raleqbidv  2759  raleqbidva  2761  omsinds  4749  cbvfo  5964  isoselem  5999  ofrfval  6284  issmo2  6533  smoeq  6534  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  nninfisollem0  7434  isacnm  7523  fzrevral2  10462  fzrevral3  10463  fzshftral  10464  fzoshftral  10606  zsupcllemstep  10611  zsupcllemex  10612  infssuzex  10615  suprzubdc  10620  nninfdcex  10621  uzsinds  10830  iseqf1olemqk  10893  seq3f1olemstep  10900  seq3f1olemp  10901  eqs1  11341  swrdspsleq  11384  pfxeq  11413  pfxsuffeqwrdeq  11415  caucvgre  11691  cvg1nlemres  11695  rexuz3  11700  resqrexlemoverl  11731  resqrexlemsqa  11734  resqrexlemex  11735  climconst  12000  climshftlemg  12012  serf0  12062  summodclem2  12093  summodc  12094  zsumdc  12095  mertenslemi1  12246  prodmodclem2  12288  prodmodc  12289  zproddc  12290  prmind2  12842  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemnn0  13257  ennnfonelemr  13258  grpidpropdg  13637  sgrppropd  13676  mndpropd  13701  nmznsg  13966  ghmnsgima  14021  cmnpropd  14048  rngpropd  14194  ringpropd  14281  lsspropdg  14705  isridlrng  14756  mplvalcoe  14971  lmfval  15184  lmconst  15207  cncnp  15221  metss  15485  sin0pilem2  15773  fsumdvdsmul  15985  2sqlem10  16124  usgruspgrben  16307  wlkeq  16475  wlkl1loop  16479  uspgr2wlkeq  16486  upgr2wlkdc  16498  clwwlkccatlem  16521  clwwlknp  16538  clwwlkn1  16539  clwwlkn2  16542  nninfsellemdc  16914  nninfself  16917  nninfsellemeqinf  16920  nninfomni  16923