Theorem rspcv 2925

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcv	⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcv

Step	Hyp	Ref	Expression
1		nfv 1581	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspc 2923	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823

This theorem is used by:  rspccv  2926  rspcva  2927  rspccva  2928  rspcdva  2934  rspc3v  2946  rr19.3v  2965  rr19.28v  2966  rspsbc  3135  rspc2vd  3216  intmin  3990  ralxfrALT  4613  ontr2exmid  4672  reg2exmidlema  4681  0elsucexmid  4712  funcnvuni  5450  acexmidlemcase  6080  suppfnss  6497  tfrlem1  6579  tfrlem9  6590  oawordriexmid  6743  nneneq  7158  diffitest  7191  xpfi  7239  ordiso2  7376  exmidontriimlem3  7580  prnmaxl  7856  prnminu  7857  cauappcvgprlemm  8013  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgsrlemcl  8157  caucvgsrlemfv  8159  caucvgsr  8170  axcaucvglemres  8267  lbreu  9278  nnsub  9346  supinfneg  10005  infsupneg  10006  ublbneg  10023  fzrevral  10523  zsupcllemex  10674  seq3caopr3  10943  seq3id3  10976  ccatalpha  11397  wrdind  11510  wrd2ind  11511  reuccatpfxs1lem  11534  recan  11892  cau3lem  11897  caubnd2  11900  climshftlemg  12087  subcn2  12096  climcau  12132  serf0  12137  sumdc  12143  isumrpcl  12280  clim2prod  12325  prodmodclem2  12363  ndvdssub  12716  dfgcd3  12806  dfgcd2  12810  coprmgcdb  12885  coprmdvds1  12888  nprm  12920  dvdsprm  12935  coprm  12942  sqrt2irr  12960  pcmpt  13145  pcmptdvds  13147  pcfac  13152  prmpwdvds  13157  lidrididd  13755  dfgrp2  13885  grpidinv2  13916  dfgrp3mlem  13956  issubg4m  14049  srgrz  14372  srglz  14373  srgisid  14374  rrgeq0i  14656  islmodd  14713  rmodislmod  14772  rnglidlmcl  14901  cnpnei  15411  lmss  15438  txlm  15471  psmet0  15519  metss  15686  metcnp3  15703  mulc1cncf  15781  cncfco  15783  chtqub  16257  2sqlem6  16405  2sqlem10  16410  usgruspgrben  16593  wlk1walkdom  16766  wlkres  16786  clwwlkccatlem  16807  clwwlkext2edg  16829  lealltlt1  16917  lealltlt2  16918  bj-indsuc  17120  bj-inf2vnlem2  17163  pw1dceq  17201  wexmiddc  17208  rirrdisj  17251  trirec0  17260  iswomni0  17268  neap0mkv  17286