Theorem rspcv 2826

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 1516	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspc 2824	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343   ∈ wcel 2136  ∀wral 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-v 2728

This theorem is referenced by:  rspccv  2827  rspcva  2828  rspccva  2829  rspcdva  2835  rspc3v  2846  rr19.3v  2865  rr19.28v  2866  rspsbc  3033  intmin  3844  ralxfrALT  4445  ontr2exmid  4502  reg2exmidlema  4511  0elsucexmid  4542  funcnvuni  5257  acexmidlemcase  5837  tfrlem1  6276  tfrlem9  6287  oawordriexmid  6438  nneneq  6823  diffitest  6853  xpfi  6895  ordiso2  7000  exmidontriimlem3  7179  prnmaxl  7429  prnminu  7430  cauappcvgprlemm  7586  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgsrlemcl  7730  caucvgsrlemfv  7732  caucvgsr  7743  axcaucvglemres  7840  lbreu  8840  nnsub  8896  supinfneg  9533  infsupneg  9534  ublbneg  9551  fzrevral  10040  seq3caopr3  10416  seq3id3  10442  recan  11051  cau3lem  11056  caubnd2  11059  climshftlemg  11243  subcn2  11252  climcau  11288  serf0  11293  sumdc  11299  isumrpcl  11435  clim2prod  11480  prodmodclem2  11518  ndvdssub  11867  zsupcllemex  11879  dfgcd3  11943  dfgcd2  11947  coprmgcdb  12020  coprmdvds1  12023  nprm  12055  dvdsprm  12069  coprm  12076  sqrt2irr  12094  pcmpt  12273  pcmptdvds  12275  pcfac  12280  prmpwdvds  12285  lidrididd  12613  cnpnei  12869  lmss  12896  txlm  12929  psmet0  12977  metss  13144  metcnp3  13161  mulc1cncf  13226  cncfco  13228  2sqlem6  13606  2sqlem10  13611  bj-indsuc  13820  bj-inf2vnlem2  13863  trirec0  13933  iswomni0  13940