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 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∀wral 2528

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 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 theorem 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 referenced by:  rspccv  2926  rspcva  2927  rspccva  2928  rspcdva  2934  rspc3v  2946  rr19.3v  2965  rr19.28v  2966  rspsbc  3135  rspc2vd  3216  intmin  3985  ralxfrALT  4608  ontr2exmid  4667  reg2exmidlema  4676  0elsucexmid  4707  funcnvuni  5445  acexmidlemcase  6070  suppfnss  6487  tfrlem1  6569  tfrlem9  6580  oawordriexmid  6733  nneneq  7148  diffitest  7181  xpfi  7229  ordiso2  7365  exmidontriimlem3  7569  prnmaxl  7845  prnminu  7846  cauappcvgprlemm  8002  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgsrlemcl  8146  caucvgsrlemfv  8148  caucvgsr  8159  axcaucvglemres  8256  lbreu  9265  nnsub  9322  supinfneg  9974  infsupneg  9975  ublbneg  9992  fzrevral  10490  zsupcllemex  10641  seq3caopr3  10906  seq3id3  10939  ccatalpha  11359  wrdind  11472  wrd2ind  11473  reuccatpfxs1lem  11496  recan  11853  cau3lem  11858  caubnd2  11861  climshftlemg  12046  subcn2  12055  climcau  12091  serf0  12096  sumdc  12102  isumrpcl  12239  clim2prod  12284  prodmodclem2  12322  ndvdssub  12675  dfgcd3  12765  dfgcd2  12769  coprmgcdb  12844  coprmdvds1  12847  nprm  12879  dvdsprm  12893  coprm  12900  sqrt2irr  12918  pcmpt  13100  pcmptdvds  13102  pcfac  13107  prmpwdvds  13112  lidrididd  13679  dfgrp2  13809  grpidinv2  13840  dfgrp3mlem  13880  issubg4m  13973  srgrz  14262  srglz  14263  srgisid  14264  rrgeq0i  14545  islmodd  14602  rmodislmod  14660  rnglidlmcl  14789  cnpnei  15243  lmss  15270  txlm  15303  psmet0  15351  metss  15518  metcnp3  15535  mulc1cncf  15613  cncfco  15615  2sqlem6  16153  2sqlem10  16158  usgruspgrben  16341  wlk1walkdom  16514  wlkres  16534  clwwlkccatlem  16555  clwwlkext2edg  16577  lealltlt1  16665  lealltlt2  16666  bj-indsuc  16868  bj-inf2vnlem2  16911  pw1dceq  16948  trirec0  16998  iswomni0  17006  neap0mkv  17024