Theorem rspcv 2697

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

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1284   ∈ wcel 1433  ∀wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-v 2603

This theorem is referenced by:  rspccv  2698  rspcva  2699  rspccva  2700  rspcda  2706  rspc3v  2716  rr19.3v  2733  rr19.28v  2734  rspsbc  2896  intmin  3656  frirrg  4105  ralxfrALT  4217  ontr2exmid  4268  reg2exmidlema  4277  0elsucexmid  4308  wetriext  4319  funcnvuni  4988  acexmidlemcase  5527  grprinvlem  5715  grprinvd  5716  caofref  5752  tfrlem1  5946  tfrlem5  5953  tfrlem9  5958  rdgon  5996  nneneq  6343  diffitest  6371  ordiso2  6446  prltlu  6677  prnmaxl  6678  prnminu  6679  cauappcvgprlemm  6835  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemm  6858  caucvgprprlemml  6884  caucvgsrlemcl  6965  caucvgsrlemfv  6967  caucvgsr  6978  axcaucvglemres  7065  lbreu  8023  nnsub  8077  supinfneg  8683  infsupneg  8684  ublbneg  8698  fzrevral  9122  iseqovex  9439  iseqval  9440  iseqfn  9441  iseq1  9442  iseqcl  9443  iseqp1  9445  iseqfveq2  9448  iseqfveq  9450  iseqfeq  9451  iseqshft2  9452  monoord  9455  monoord2  9456  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqid3s  9466  iseqid  9467  iseqhomo  9468  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniq  9881  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  recan  9995  cau3lem  10000  caubnd2  10003  climi  10126  climshftlemg  10141  climcn1  10147  subcn2  10150  climcau  10184  serif0  10189  ndvdssub  10330  zsupcllemex  10342  bezoutlemmain  10387  dfgcd3  10399  dfgcd2  10403  coprmgcdb  10470  coprmdvds1  10473  prmind2  10502  nprm  10505  dvdsprm  10518  coprm  10523  sqrt2irr  10541  bj-indsuc  10723  bj-inf2vnlem2  10766