Theorem rspcv 2837

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148  ∀wral 2455

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2739

This theorem is referenced by:  rspccv  2838  rspcva  2839  rspccva  2840  rspcdva  2846  rspc3v  2857  rr19.3v  2876  rr19.28v  2877  rspsbc  3045  rspc2vd  3125  intmin  3863  ralxfrALT  4465  ontr2exmid  4522  reg2exmidlema  4531  0elsucexmid  4562  funcnvuni  5282  acexmidlemcase  5865  tfrlem1  6304  tfrlem9  6315  oawordriexmid  6466  nneneq  6852  diffitest  6882  xpfi  6924  ordiso2  7029  exmidontriimlem3  7217  prnmaxl  7482  prnminu  7483  cauappcvgprlemm  7639  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  caucvgsrlemcl  7783  caucvgsrlemfv  7785  caucvgsr  7796  axcaucvglemres  7893  lbreu  8896  nnsub  8952  supinfneg  9589  infsupneg  9590  ublbneg  9607  fzrevral  10098  seq3caopr3  10474  seq3id3  10500  recan  11109  cau3lem  11114  caubnd2  11117  climshftlemg  11301  subcn2  11310  climcau  11346  serf0  11351  sumdc  11357  isumrpcl  11493  clim2prod  11538  prodmodclem2  11576  ndvdssub  11925  zsupcllemex  11937  dfgcd3  12001  dfgcd2  12005  coprmgcdb  12078  coprmdvds1  12081  nprm  12113  dvdsprm  12127  coprm  12134  sqrt2irr  12152  pcmpt  12331  pcmptdvds  12333  pcfac  12338  prmpwdvds  12343  lidrididd  12731  dfgrp2  12830  grpidinv2  12856  dfgrp3mlem  12896  issubg4m  12979  srgrz  13067  srglz  13068  srgisid  13069  cnpnei  13501  lmss  13528  txlm  13561  psmet0  13609  metss  13776  metcnp3  13793  mulc1cncf  13858  cncfco  13860  2sqlem6  14238  2sqlem10  14243  bj-indsuc  14451  bj-inf2vnlem2  14494  trirec0  14563  iswomni0  14570  neap0mkv  14587