Theorem rspcv 2903

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801

This theorem is referenced by:  rspccv  2904  rspcva  2905  rspccva  2906  rspcdva  2912  rspc3v  2923  rr19.3v  2942  rr19.28v  2943  rspsbc  3112  rspc2vd  3193  intmin  3943  ralxfrALT  4558  ontr2exmid  4617  reg2exmidlema  4626  0elsucexmid  4657  funcnvuni  5390  acexmidlemcase  6002  tfrlem1  6460  tfrlem9  6471  oawordriexmid  6624  nneneq  7026  diffitest  7057  xpfi  7105  ordiso2  7213  exmidontriimlem3  7416  prnmaxl  7686  prnminu  7687  cauappcvgprlemm  7843  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsr  8000  axcaucvglemres  8097  lbreu  9103  nnsub  9160  supinfneg  9802  infsupneg  9803  ublbneg  9820  fzrevral  10313  zsupcllemex  10462  seq3caopr3  10725  seq3id3  10758  ccatalpha  11161  wrdind  11269  wrd2ind  11270  reuccatpfxs1lem  11293  recan  11635  cau3lem  11640  caubnd2  11643  climshftlemg  11828  subcn2  11837  climcau  11873  serf0  11878  sumdc  11884  isumrpcl  12020  clim2prod  12065  prodmodclem2  12103  ndvdssub  12456  dfgcd3  12546  dfgcd2  12550  coprmgcdb  12625  coprmdvds1  12628  nprm  12660  dvdsprm  12674  coprm  12681  sqrt2irr  12699  pcmpt  12881  pcmptdvds  12883  pcfac  12888  prmpwdvds  12893  lidrididd  13430  dfgrp2  13575  grpidinv2  13606  dfgrp3mlem  13646  issubg4m  13745  srgrz  13962  srglz  13963  srgisid  13964  rrgeq0i  14243  islmodd  14272  rmodislmod  14330  rnglidlmcl  14459  cnpnei  14908  lmss  14935  txlm  14968  psmet0  15016  metss  15183  metcnp3  15200  mulc1cncf  15278  cncfco  15280  2sqlem6  15814  2sqlem10  15819  usgruspgrben  15999  wlk1walkdom  16100  wlkres  16118  clwwlkccatlem  16137  bj-indsuc  16346  bj-inf2vnlem2  16389  pw1dceq  16429  trirec0  16472  iswomni0  16479  neap0mkv  16497