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  6013  tfrlem1  6474  tfrlem9  6485  oawordriexmid  6638  nneneq  7043  diffitest  7076  xpfi  7124  ordiso2  7234  exmidontriimlem3  7438  prnmaxl  7708  prnminu  7709  cauappcvgprlemm  7865  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsr  8022  axcaucvglemres  8119  lbreu  9125  nnsub  9182  supinfneg  9829  infsupneg  9830  ublbneg  9847  fzrevral  10340  zsupcllemex  10491  seq3caopr3  10754  seq3id3  10787  ccatalpha  11194  wrdind  11307  wrd2ind  11308  reuccatpfxs1lem  11331  recan  11687  cau3lem  11692  caubnd2  11695  climshftlemg  11880  subcn2  11889  climcau  11925  serf0  11930  sumdc  11936  isumrpcl  12073  clim2prod  12118  prodmodclem2  12156  ndvdssub  12509  dfgcd3  12599  dfgcd2  12603  coprmgcdb  12678  coprmdvds1  12681  nprm  12713  dvdsprm  12727  coprm  12734  sqrt2irr  12752  pcmpt  12934  pcmptdvds  12936  pcfac  12941  prmpwdvds  12946  lidrididd  13483  dfgrp2  13628  grpidinv2  13659  dfgrp3mlem  13699  issubg4m  13798  srgrz  14016  srglz  14017  srgisid  14018  rrgeq0i  14297  islmodd  14326  rmodislmod  14384  rnglidlmcl  14513  cnpnei  14962  lmss  14989  txlm  15022  psmet0  15070  metss  15237  metcnp3  15254  mulc1cncf  15332  cncfco  15334  2sqlem6  15868  2sqlem10  15873  usgruspgrben  16056  wlk1walkdom  16229  wlkres  16249  clwwlkccatlem  16270  clwwlkext2edg  16292  bj-indsuc  16574  bj-inf2vnlem2  16617  pw1dceq  16656  trirec0  16699  iswomni0  16707  neap0mkv  16725