Theorem rspcv 2904

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802

This theorem is referenced by:  rspccv  2905  rspcva  2906  rspccva  2907  rspcdva  2913  rspc3v  2924  rr19.3v  2943  rr19.28v  2944  rspsbc  3113  rspc2vd  3194  intmin  3946  ralxfrALT  4562  ontr2exmid  4621  reg2exmidlema  4630  0elsucexmid  4661  funcnvuni  5396  acexmidlemcase  6008  tfrlem1  6469  tfrlem9  6480  oawordriexmid  6633  nneneq  7038  diffitest  7069  xpfi  7117  ordiso2  7225  exmidontriimlem3  7428  prnmaxl  7698  prnminu  7699  cauappcvgprlemm  7855  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgsrlemcl  7999  caucvgsrlemfv  8001  caucvgsr  8012  axcaucvglemres  8109  lbreu  9115  nnsub  9172  supinfneg  9819  infsupneg  9820  ublbneg  9837  fzrevral  10330  zsupcllemex  10480  seq3caopr3  10743  seq3id3  10776  ccatalpha  11180  wrdind  11293  wrd2ind  11294  reuccatpfxs1lem  11317  recan  11660  cau3lem  11665  caubnd2  11668  climshftlemg  11853  subcn2  11862  climcau  11898  serf0  11903  sumdc  11909  isumrpcl  12045  clim2prod  12090  prodmodclem2  12128  ndvdssub  12481  dfgcd3  12571  dfgcd2  12575  coprmgcdb  12650  coprmdvds1  12653  nprm  12685  dvdsprm  12699  coprm  12706  sqrt2irr  12724  pcmpt  12906  pcmptdvds  12908  pcfac  12913  prmpwdvds  12918  lidrididd  13455  dfgrp2  13600  grpidinv2  13631  dfgrp3mlem  13671  issubg4m  13770  srgrz  13987  srglz  13988  srgisid  13989  rrgeq0i  14268  islmodd  14297  rmodislmod  14355  rnglidlmcl  14484  cnpnei  14933  lmss  14960  txlm  14993  psmet0  15041  metss  15208  metcnp3  15225  mulc1cncf  15303  cncfco  15305  2sqlem6  15839  2sqlem10  15844  usgruspgrben  16025  wlk1walkdom  16156  wlkres  16174  clwwlkccatlem  16195  clwwlkext2edg  16217  bj-indsuc  16459  bj-inf2vnlem2  16502  pw1dceq  16541  trirec0  16584  iswomni0  16591  neap0mkv  16609