Theorem rspcv 2835

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2146  ∀wral 2453

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-v 2737

This theorem is referenced by:  rspccv  2836  rspcva  2837  rspccva  2838  rspcdva  2844  rspc3v  2855  rr19.3v  2874  rr19.28v  2875  rspsbc  3043  rspc2vd  3123  intmin  3860  ralxfrALT  4461  ontr2exmid  4518  reg2exmidlema  4527  0elsucexmid  4558  funcnvuni  5277  acexmidlemcase  5860  tfrlem1  6299  tfrlem9  6310  oawordriexmid  6461  nneneq  6847  diffitest  6877  xpfi  6919  ordiso2  7024  exmidontriimlem3  7212  prnmaxl  7462  prnminu  7463  cauappcvgprlemm  7619  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  caucvgsrlemcl  7763  caucvgsrlemfv  7765  caucvgsr  7776  axcaucvglemres  7873  lbreu  8875  nnsub  8931  supinfneg  9568  infsupneg  9569  ublbneg  9586  fzrevral  10075  seq3caopr3  10451  seq3id3  10477  recan  11086  cau3lem  11091  caubnd2  11094  climshftlemg  11278  subcn2  11287  climcau  11323  serf0  11328  sumdc  11334  isumrpcl  11470  clim2prod  11515  prodmodclem2  11553  ndvdssub  11902  zsupcllemex  11914  dfgcd3  11978  dfgcd2  11982  coprmgcdb  12055  coprmdvds1  12058  nprm  12090  dvdsprm  12104  coprm  12111  sqrt2irr  12129  pcmpt  12308  pcmptdvds  12310  pcfac  12315  prmpwdvds  12320  lidrididd  12667  dfgrp2  12764  grpidinv2  12790  dfgrp3mlem  12829  srgrz  12964  srglz  12965  srgisid  12966  cnpnei  13290  lmss  13317  txlm  13350  psmet0  13398  metss  13565  metcnp3  13582  mulc1cncf  13647  cncfco  13649  2sqlem6  14027  2sqlem10  14032  bj-indsuc  14240  bj-inf2vnlem2  14283  trirec0  14353  iswomni0  14360