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  3895  ralxfrALT  4503  ontr2exmid  4562  reg2exmidlema  4571  0elsucexmid  4602  funcnvuni  5328  acexmidlemcase  5920  tfrlem1  6375  tfrlem9  6386  oawordriexmid  6537  nneneq  6927  diffitest  6957  xpfi  7002  ordiso2  7110  exmidontriimlem3  7306  prnmaxl  7572  prnminu  7573  cauappcvgprlemm  7729  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgsrlemcl  7873  caucvgsrlemfv  7875  caucvgsr  7886  axcaucvglemres  7983  lbreu  8989  nnsub  9046  supinfneg  9686  infsupneg  9687  ublbneg  9704  fzrevral  10197  zsupcllemex  10337  seq3caopr3  10600  seq3id3  10633  recan  11291  cau3lem  11296  caubnd2  11299  climshftlemg  11484  subcn2  11493  climcau  11529  serf0  11534  sumdc  11540  isumrpcl  11676  clim2prod  11721  prodmodclem2  11759  ndvdssub  12112  dfgcd3  12202  dfgcd2  12206  coprmgcdb  12281  coprmdvds1  12284  nprm  12316  dvdsprm  12330  coprm  12337  sqrt2irr  12355  pcmpt  12537  pcmptdvds  12539  pcfac  12544  prmpwdvds  12549  lidrididd  13084  dfgrp2  13229  grpidinv2  13260  dfgrp3mlem  13300  issubg4m  13399  srgrz  13616  srglz  13617  srgisid  13618  rrgeq0i  13896  islmodd  13925  rmodislmod  13983  rnglidlmcl  14112  cnpnei  14539  lmss  14566  txlm  14599  psmet0  14647  metss  14814  metcnp3  14831  mulc1cncf  14909  cncfco  14911  2sqlem6  15445  2sqlem10  15450  bj-indsuc  15658  bj-inf2vnlem2  15701  trirec0  15775  iswomni0  15782  neap0mkv  15800