Theorem rspcv 2877

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2177  ∀wral 2485

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775

This theorem is referenced by:  rspccv  2878  rspcva  2879  rspccva  2880  rspcdva  2886  rspc3v  2897  rr19.3v  2916  rr19.28v  2917  rspsbc  3085  rspc2vd  3166  intmin  3911  ralxfrALT  4522  ontr2exmid  4581  reg2exmidlema  4590  0elsucexmid  4621  funcnvuni  5352  acexmidlemcase  5952  tfrlem1  6407  tfrlem9  6418  oawordriexmid  6569  nneneq  6969  diffitest  6999  xpfi  7044  ordiso2  7152  exmidontriimlem3  7351  prnmaxl  7621  prnminu  7622  cauappcvgprlemm  7778  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  caucvgsrlemcl  7922  caucvgsrlemfv  7924  caucvgsr  7935  axcaucvglemres  8032  lbreu  9038  nnsub  9095  supinfneg  9736  infsupneg  9737  ublbneg  9754  fzrevral  10247  zsupcllemex  10395  seq3caopr3  10658  seq3id3  10691  wrdind  11198  wrd2ind  11199  recan  11495  cau3lem  11500  caubnd2  11503  climshftlemg  11688  subcn2  11697  climcau  11733  serf0  11738  sumdc  11744  isumrpcl  11880  clim2prod  11925  prodmodclem2  11963  ndvdssub  12316  dfgcd3  12406  dfgcd2  12410  coprmgcdb  12485  coprmdvds1  12488  nprm  12520  dvdsprm  12534  coprm  12541  sqrt2irr  12559  pcmpt  12741  pcmptdvds  12743  pcfac  12748  prmpwdvds  12753  lidrididd  13289  dfgrp2  13434  grpidinv2  13465  dfgrp3mlem  13505  issubg4m  13604  srgrz  13821  srglz  13822  srgisid  13823  rrgeq0i  14101  islmodd  14130  rmodislmod  14188  rnglidlmcl  14317  cnpnei  14766  lmss  14793  txlm  14826  psmet0  14874  metss  15041  metcnp3  15058  mulc1cncf  15136  cncfco  15138  2sqlem6  15672  2sqlem10  15677  bj-indsuc  16002  bj-inf2vnlem2  16045  trirec0  16124  iswomni0  16131  neap0mkv  16149