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  7308  prnmaxl  7574  prnminu  7575  cauappcvgprlemm  7731  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgsrlemcl  7875  caucvgsrlemfv  7877  caucvgsr  7888  axcaucvglemres  7985  lbreu  8991  nnsub  9048  supinfneg  9688  infsupneg  9689  ublbneg  9706  fzrevral  10199  zsupcllemex  10339  seq3caopr3  10602  seq3id3  10635  recan  11293  cau3lem  11298  caubnd2  11301  climshftlemg  11486  subcn2  11495  climcau  11531  serf0  11536  sumdc  11542  isumrpcl  11678  clim2prod  11723  prodmodclem2  11761  ndvdssub  12114  dfgcd3  12204  dfgcd2  12208  coprmgcdb  12283  coprmdvds1  12286  nprm  12318  dvdsprm  12332  coprm  12339  sqrt2irr  12357  pcmpt  12539  pcmptdvds  12541  pcfac  12546  prmpwdvds  12551  lidrididd  13086  dfgrp2  13231  grpidinv2  13262  dfgrp3mlem  13302  issubg4m  13401  srgrz  13618  srglz  13619  srgisid  13620  rrgeq0i  13898  islmodd  13927  rmodislmod  13985  rnglidlmcl  14114  cnpnei  14563  lmss  14590  txlm  14623  psmet0  14671  metss  14838  metcnp3  14855  mulc1cncf  14933  cncfco  14935  2sqlem6  15469  2sqlem10  15474  bj-indsuc  15682  bj-inf2vnlem2  15725  trirec0  15801  iswomni0  15808  neap0mkv  15826