Theorem rspcv 2864

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765

This theorem is referenced by:  rspccv  2865  rspcva  2866  rspccva  2867  rspcdva  2873  rspc3v  2884  rr19.3v  2903  rr19.28v  2904  rspsbc  3072  rspc2vd  3153  intmin  3894  ralxfrALT  4502  ontr2exmid  4561  reg2exmidlema  4570  0elsucexmid  4601  funcnvuni  5327  acexmidlemcase  5917  tfrlem1  6366  tfrlem9  6377  oawordriexmid  6528  nneneq  6918  diffitest  6948  xpfi  6993  ordiso2  7101  exmidontriimlem3  7290  prnmaxl  7555  prnminu  7556  cauappcvgprlemm  7712  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgsrlemcl  7856  caucvgsrlemfv  7858  caucvgsr  7869  axcaucvglemres  7966  lbreu  8972  nnsub  9029  supinfneg  9669  infsupneg  9670  ublbneg  9687  fzrevral  10180  zsupcllemex  10320  seq3caopr3  10583  seq3id3  10616  recan  11274  cau3lem  11279  caubnd2  11282  climshftlemg  11467  subcn2  11476  climcau  11512  serf0  11517  sumdc  11523  isumrpcl  11659  clim2prod  11704  prodmodclem2  11742  ndvdssub  12095  dfgcd3  12177  dfgcd2  12181  coprmgcdb  12256  coprmdvds1  12259  nprm  12291  dvdsprm  12305  coprm  12312  sqrt2irr  12330  pcmpt  12512  pcmptdvds  12514  pcfac  12519  prmpwdvds  12524  lidrididd  13025  dfgrp2  13159  grpidinv2  13190  dfgrp3mlem  13230  issubg4m  13323  srgrz  13540  srglz  13541  srgisid  13542  rrgeq0i  13820  islmodd  13849  rmodislmod  13907  rnglidlmcl  14036  cnpnei  14455  lmss  14482  txlm  14515  psmet0  14563  metss  14730  metcnp3  14747  mulc1cncf  14825  cncfco  14827  2sqlem6  15361  2sqlem10  15366  bj-indsuc  15574  bj-inf2vnlem2  15617  trirec0  15688  iswomni0  15695  neap0mkv  15713