Theorem rspcv 2872

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372   ∈ wcel 2175  ∀wral 2483

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-v 2773

This theorem is referenced by:  rspccv  2873  rspcva  2874  rspccva  2875  rspcdva  2881  rspc3v  2892  rr19.3v  2911  rr19.28v  2912  rspsbc  3080  rspc2vd  3161  intmin  3904  ralxfrALT  4513  ontr2exmid  4572  reg2exmidlema  4581  0elsucexmid  4612  funcnvuni  5342  acexmidlemcase  5938  tfrlem1  6393  tfrlem9  6404  oawordriexmid  6555  nneneq  6953  diffitest  6983  xpfi  7028  ordiso2  7136  exmidontriimlem3  7334  prnmaxl  7600  prnminu  7601  cauappcvgprlemm  7757  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgsrlemcl  7901  caucvgsrlemfv  7903  caucvgsr  7914  axcaucvglemres  8011  lbreu  9017  nnsub  9074  supinfneg  9715  infsupneg  9716  ublbneg  9733  fzrevral  10226  zsupcllemex  10371  seq3caopr3  10634  seq3id3  10667  recan  11362  cau3lem  11367  caubnd2  11370  climshftlemg  11555  subcn2  11564  climcau  11600  serf0  11605  sumdc  11611  isumrpcl  11747  clim2prod  11792  prodmodclem2  11830  ndvdssub  12183  dfgcd3  12273  dfgcd2  12277  coprmgcdb  12352  coprmdvds1  12355  nprm  12387  dvdsprm  12401  coprm  12408  sqrt2irr  12426  pcmpt  12608  pcmptdvds  12610  pcfac  12615  prmpwdvds  12620  lidrididd  13156  dfgrp2  13301  grpidinv2  13332  dfgrp3mlem  13372  issubg4m  13471  srgrz  13688  srglz  13689  srgisid  13690  rrgeq0i  13968  islmodd  13997  rmodislmod  14055  rnglidlmcl  14184  cnpnei  14633  lmss  14660  txlm  14693  psmet0  14741  metss  14908  metcnp3  14925  mulc1cncf  15003  cncfco  15005  2sqlem6  15539  2sqlem10  15544  bj-indsuc  15797  bj-inf2vnlem2  15840  trirec0  15916  iswomni0  15923  neap0mkv  15941