Theorem rspcv 2754

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1312   ∈ wcel 1461  ∀wral 2388

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-v 2657

This theorem is referenced by:  rspccv  2755  rspcva  2756  rspccva  2757  rspcdva  2763  rspc3v  2773  rr19.3v  2791  rr19.28v  2792  rspsbc  2957  intmin  3755  ralxfrALT  4346  ontr2exmid  4398  reg2exmidlema  4407  0elsucexmid  4438  funcnvuni  5148  acexmidlemcase  5721  tfrlem1  6156  tfrlem9  6167  oawordriexmid  6317  nneneq  6701  diffitest  6731  xpfi  6768  ordiso2  6869  prnmaxl  7237  prnminu  7238  cauappcvgprlemm  7394  cauappcvgprlemladdru  7405  cauappcvgprlemladdrl  7406  caucvgsrlemcl  7524  caucvgsrlemfv  7526  caucvgsr  7537  axcaucvglemres  7627  lbreu  8606  nnsub  8662  supinfneg  9285  infsupneg  9286  ublbneg  9300  fzrevral  9771  seq3caopr3  10140  seq3id3  10166  recan  10766  cau3lem  10771  caubnd2  10774  climshftlemg  10956  subcn2  10965  climcau  11001  serf0  11006  sumdc  11012  isumrpcl  11148  ndvdssub  11468  zsupcllemex  11480  dfgcd3  11537  dfgcd2  11541  coprmgcdb  11608  coprmdvds1  11611  nprm  11643  dvdsprm  11656  coprm  11661  sqrt2irr  11679  cnpnei  12223  lmss  12250  txlm  12283  psmet0  12309  metss  12476  metcnp3  12493  mulc1cncf  12555  cncfco  12557  bj-indsuc  12805  bj-inf2vnlem2  12848