Theorem rspcv 2830

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   ∈ wcel 2141  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732

This theorem is referenced by:  rspccv  2831  rspcva  2832  rspccva  2833  rspcdva  2839  rspc3v  2850  rr19.3v  2869  rr19.28v  2870  rspsbc  3037  rspc2vd  3117  intmin  3851  ralxfrALT  4452  ontr2exmid  4509  reg2exmidlema  4518  0elsucexmid  4549  funcnvuni  5267  acexmidlemcase  5848  tfrlem1  6287  tfrlem9  6298  oawordriexmid  6449  nneneq  6835  diffitest  6865  xpfi  6907  ordiso2  7012  exmidontriimlem3  7200  prnmaxl  7450  prnminu  7451  cauappcvgprlemm  7607  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgsrlemcl  7751  caucvgsrlemfv  7753  caucvgsr  7764  axcaucvglemres  7861  lbreu  8861  nnsub  8917  supinfneg  9554  infsupneg  9555  ublbneg  9572  fzrevral  10061  seq3caopr3  10437  seq3id3  10463  recan  11073  cau3lem  11078  caubnd2  11081  climshftlemg  11265  subcn2  11274  climcau  11310  serf0  11315  sumdc  11321  isumrpcl  11457  clim2prod  11502  prodmodclem2  11540  ndvdssub  11889  zsupcllemex  11901  dfgcd3  11965  dfgcd2  11969  coprmgcdb  12042  coprmdvds1  12045  nprm  12077  dvdsprm  12091  coprm  12098  sqrt2irr  12116  pcmpt  12295  pcmptdvds  12297  pcfac  12302  prmpwdvds  12307  lidrididd  12636  dfgrp2  12732  grpidinv2  12758  cnpnei  13013  lmss  13040  txlm  13073  psmet0  13121  metss  13288  metcnp3  13305  mulc1cncf  13370  cncfco  13372  2sqlem6  13750  2sqlem10  13755  bj-indsuc  13963  bj-inf2vnlem2  14006  trirec0  14076  iswomni0  14083