Theorem rspcv 2906

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202  ∀wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804

This theorem is referenced by:  rspccv  2907  rspcva  2908  rspccva  2909  rspcdva  2915  rspc3v  2926  rr19.3v  2945  rr19.28v  2946  rspsbc  3115  rspc2vd  3196  intmin  3948  ralxfrALT  4564  ontr2exmid  4623  reg2exmidlema  4632  0elsucexmid  4663  funcnvuni  5399  acexmidlemcase  6012  tfrlem1  6473  tfrlem9  6484  oawordriexmid  6637  nneneq  7042  diffitest  7075  xpfi  7123  ordiso2  7233  exmidontriimlem3  7437  prnmaxl  7707  prnminu  7708  cauappcvgprlemm  7864  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgsrlemcl  8008  caucvgsrlemfv  8010  caucvgsr  8021  axcaucvglemres  8118  lbreu  9124  nnsub  9181  supinfneg  9828  infsupneg  9829  ublbneg  9846  fzrevral  10339  zsupcllemex  10489  seq3caopr3  10752  seq3id3  10785  ccatalpha  11189  wrdind  11302  wrd2ind  11303  reuccatpfxs1lem  11326  recan  11669  cau3lem  11674  caubnd2  11677  climshftlemg  11862  subcn2  11871  climcau  11907  serf0  11912  sumdc  11918  isumrpcl  12054  clim2prod  12099  prodmodclem2  12137  ndvdssub  12490  dfgcd3  12580  dfgcd2  12584  coprmgcdb  12659  coprmdvds1  12662  nprm  12694  dvdsprm  12708  coprm  12715  sqrt2irr  12733  pcmpt  12915  pcmptdvds  12917  pcfac  12922  prmpwdvds  12927  lidrididd  13464  dfgrp2  13609  grpidinv2  13640  dfgrp3mlem  13680  issubg4m  13779  srgrz  13996  srglz  13997  srgisid  13998  rrgeq0i  14277  islmodd  14306  rmodislmod  14364  rnglidlmcl  14493  cnpnei  14942  lmss  14969  txlm  15002  psmet0  15050  metss  15217  metcnp3  15234  mulc1cncf  15312  cncfco  15314  2sqlem6  15848  2sqlem10  15853  usgruspgrben  16036  wlk1walkdom  16209  wlkres  16229  clwwlkccatlem  16250  clwwlkext2edg  16272  bj-indsuc  16523  bj-inf2vnlem2  16566  pw1dceq  16605  trirec0  16648  iswomni0  16655  neap0mkv  16673