Theorem rspcv 2852

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2160  ∀wral 2468

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-v 2754

This theorem is referenced by:  rspccv  2853  rspcva  2854  rspccva  2855  rspcdva  2861  rspc3v  2872  rr19.3v  2891  rr19.28v  2892  rspsbc  3060  rspc2vd  3140  intmin  3879  ralxfrALT  4485  ontr2exmid  4542  reg2exmidlema  4551  0elsucexmid  4582  funcnvuni  5304  acexmidlemcase  5892  tfrlem1  6334  tfrlem9  6345  oawordriexmid  6496  nneneq  6886  diffitest  6916  xpfi  6959  ordiso2  7065  exmidontriimlem3  7253  prnmaxl  7518  prnminu  7519  cauappcvgprlemm  7675  cauappcvgprlemladdru  7686  cauappcvgprlemladdrl  7687  caucvgsrlemcl  7819  caucvgsrlemfv  7821  caucvgsr  7832  axcaucvglemres  7929  lbreu  8933  nnsub  8989  supinfneg  9627  infsupneg  9628  ublbneg  9645  fzrevral  10137  seq3caopr3  10514  seq3id3  10540  recan  11153  cau3lem  11158  caubnd2  11161  climshftlemg  11345  subcn2  11354  climcau  11390  serf0  11395  sumdc  11401  isumrpcl  11537  clim2prod  11582  prodmodclem2  11620  ndvdssub  11970  zsupcllemex  11982  dfgcd3  12046  dfgcd2  12050  coprmgcdb  12123  coprmdvds1  12126  nprm  12158  dvdsprm  12172  coprm  12179  sqrt2irr  12197  pcmpt  12378  pcmptdvds  12380  pcfac  12385  prmpwdvds  12390  lidrididd  12861  dfgrp2  12986  grpidinv2  13017  dfgrp3mlem  13057  issubg4m  13149  srgrz  13355  srglz  13356  srgisid  13357  islmodd  13626  rmodislmod  13684  rnglidlmcl  13813  cnpnei  14196  lmss  14223  txlm  14256  psmet0  14304  metss  14471  metcnp3  14488  mulc1cncf  14553  cncfco  14555  2sqlem6  14945  2sqlem10  14950  bj-indsuc  15158  bj-inf2vnlem2  15201  trirec0  15271  iswomni0  15278  neap0mkv  15296