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  7375  exmidontriimlem3  7579  prnmaxl  7855  prnminu  7856  cauappcvgprlemm  8012  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsr  8169  axcaucvglemres  8266  lbreu  9277  nnsub  9345  supinfneg  10004  infsupneg  10005  ublbneg  10022  fzrevral  10522  zsupcllemex  10673  seq3caopr3  10941  seq3id3  10974  ccatalpha  11395  wrdind  11508  wrd2ind  11509  reuccatpfxs1lem  11532  recan  11890  cau3lem  11895  caubnd2  11898  climshftlemg  12084  subcn2  12093  climcau  12129  serf0  12134  sumdc  12140  isumrpcl  12277  clim2prod  12322  prodmodclem2  12360  ndvdssub  12713  dfgcd3  12803  dfgcd2  12807  coprmgcdb  12882  coprmdvds1  12885  nprm  12917  dvdsprm  12932  coprm  12939  sqrt2irr  12957  pcmpt  13142  pcmptdvds  13144  pcfac  13149  prmpwdvds  13154  lidrididd  13751  dfgrp2  13881  grpidinv2  13912  dfgrp3mlem  13952  issubg4m  14045  srgrz  14337  srglz  14338  srgisid  14339  rrgeq0i  14621  islmodd  14678  rmodislmod  14737  rnglidlmcl  14866  cnpnei  15369  lmss  15396  txlm  15429  psmet0  15477  metss  15644  metcnp3  15661  mulc1cncf  15739  cncfco  15741  2sqlem6  16337  2sqlem10  16342  usgruspgrben  16525  wlk1walkdom  16698  wlkres  16718  clwwlkccatlem  16739  clwwlkext2edg  16761  lealltlt1  16849  lealltlt2  16850  bj-indsuc  17052  bj-inf2vnlem2  17095  pw1dceq  17133  wexmiddc  17140  trirec0  17191  iswomni0  17199  neap0mkv  17217