Theorem rspcv 3533

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1508   ∈ wcel 2051  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ral 3095  df-v 3419

This theorem is referenced by:  rspccv  3534  rspcva  3535  rspccva  3536  rspcdva  3543  rspc2v  3550  rspc3v  3553  rr19.3v  3577  rr19.28v  3578  rspsbc  3767  intmin  4774  ralxfrALT  5173  somo  5366  fr2nr  5389  weniso  6936  fr3nr  7316  limuni3  7389  tfinds  7396  funcnvuni  7457  suppfnss  7664  onnseq  7791  smo11  7811  tfrlem9  7831  tz7.49  7890  omeulem1  8015  oeordi  8020  nneneq  8502  frfi  8564  unblem2  8572  unbnn2  8576  xpfi  8590  ordiso2  8780  cantnflem1  8952  rankunb  9079  tcrank  9113  carduni  9210  dfac8alem  9255  alephinit  9321  aceq3lem  9346  dfac5  9354  dfac12r  9372  dfac12k  9373  pwsdompw  9430  cflm  9476  isf32lem1  9579  isf32lem2  9580  isf34lem4  9603  hsmexlem4  9655  axcc3  9664  domtriomlem  9668  axdc3lem2  9677  axdc4lem  9681  axcclem  9683  axdclem  9745  alephval2  9798  winainflem  9919  eltskm  10069  squeeze0  11350  fiminreOLD  11397  lbreu  11398  nnsub  11490  ublbneg  12153  zmax  12165  zbtwnre  12166  xrub  12527  infmremnf  12558  infmrp1  12559  fzrevral  12814  axdc4uzlem  13172  faclbnd4lem4  13477  ccatalpha  13762  wrdind  13921  wrdindOLD  13922  wrd2ind  13923  wrd2indOLD  13924  reuccats1lemOLD  13926  reuccatpfxs1lem  13961  recan  14563  cau3lem  14581  caubnd2  14584  climrlim2  14771  climshftlem  14798  rlimcld2  14802  subcn2  14818  isercoll  14891  climcau  14894  serf0  14904  iseralt  14908  isumrpcl  15064  clim2prod  15110  ntrivcvgfvn0  15121  sqrt2irr  15468  ndvdssub  15626  dfgcd2  15756  lcmf  15839  lcmfunsnlem1  15843  lcmfunsnlem2lem1  15844  lcmfunsnlem2lem2  15845  lcmfdvdsb  15849  coprmgcdb  15855  coprmdvds1  15858  coprmprod  15867  coprmproddvdslem  15868  nprm  15894  dvdsprm  15909  coprm  15917  pcmpt  16090  pcmptdvds  16092  pcfac  16097  prmpwdvds  16102  unbenlem  16106  vdwlem10  16188  vdwlem13  16191  vdwnnlem1  16193  prmdvdsprmop  16241  prmgaplem7  16255  catideu  16816  initoid  17135  termoid  17136  initoeu1  17141  termoeu1  17148  isdrs2  17419  lublecllem  17468  lubun  17603  sgrp2rid2ex  17895  dfgrp2  17928  grpidinv2  17957  dfgrp3lem  17996  issubg4  18094  efgi  18615  efgi2  18621  dprdss  18913  srgrz  19011  srglz  19012  srgisid  19013  f1rhm0to0ALT  19229  islmodd  19374  rmodislmod  19436  islmhm2  19544  rrgeq0i  19795  mvrf1  19931  cply1mul  20180  ip2eq  20514  isclo2  21415  cnpnei  21591  cncls  21601  lmss  21625  cnt0  21673  isnrm2  21685  isreg2  21704  tgcmp  21728  uncmp  21730  dfconn2  21746  1stcclb  21771  2ndcctbss  21782  comppfsc  21859  kgencn2  21884  ptpjpre1  21898  txlm  21975  kqfvima  22057  kqt0lem  22063  isr0  22064  nrmr0reg  22076  fgss2  22201  isufil2  22235  cfinufil  22255  flimopn  22302  fbflim2  22304  flfneii  22319  cnpflf  22328  fclssscls  22345  fclsnei  22346  fclsrest  22351  flimfnfcls  22355  fclscmp  22357  isfcf  22361  fcfnei  22362  alexsubALTlem3  22376  alexsubALTlem4  22377  alexsubALT  22378  tsmsgsum  22465  tsmsres  22470  tsmsxplem1  22479  ustincl  22534  ustdiag  22535  ustinvel  22536  ustexhalf  22537  cfiluexsm  22617  psmet0  22636  prdsbl  22819  metss  22836  metcnp3  22868  isngp4  22939  nmoi  23055  mulc1cncf  23231  cncfco  23233  lebnumii  23288  iscfil3  23594  iscau2  23598  iscau4  23600  equivcfil  23620  equivcau  23621  lmcau  23634  ismbf  23947  ellimc3  24195  lhop1  24329  dvfsumlem4  24344  dvfsum2  24349  dgrco  24583  fta1  24615  aalioulem2  24640  aalioulem4  24642  ulmclm  24693  ulmshftlem  24695  ulmcaulem  24700  ulmcau  24701  ulmcn  24705  cxploglim  25272  ftalem3  25369  chtub  25505  dchrelbasd  25532  2sqlem6  25716  2sqlem10  25721  dchrisumlema  25781  dchrisumlem2  25783  dchrisumlem3  25784  dchrvmasumlem2  25791  pntpbnd1  25879  pntibnd  25886  pntleml  25904  brbtwn2  26409  colinearalg  26414  axcontlem4  26471  usgruspgrb  26684  cusgredg  26924  cusgrres  26948  usgredgsscusgredg  26959  fusgrn0degnn0  26999  wlk1walk  27138  wlkres  27171  wlkresOLD  27173  wlkp1lem6  27181  wlkdlem2  27186  upgrwlkdvdelem  27240  pthdlem2lem  27271  lfgrn1cycl  27306  wwlksnredwwlkn  27399  wwlksnredwwlknOLD  27400  wwlksnextproplem2  27426  wwlksnextproplem2OLD  27427  clwwlkccatlem  27510  clwlkclwwlkf1lem3  27530  clwlkclwwlkf1lem3OLD  27531  clwwisshclwwslemlem  27543  clwwlkf1OLD  27581  clwwlkf1  27586  clwwlkext2edg  27594  rspc2vd  27814  3cyclfrgrrn1  27834  n4cyclfrgr  27840  frgrwopregasn  27865  frgrwopregbsn  27866  isgrpo  28066  blocnilem  28373  ip2eqi  28426  htthlem  28488  hial0  28673  hial02  28674  hial2eq  28677  ocorth  28864  h1de2i  29126  pjjsi  29273  lnopunilem1  29583  lnophmlem1  29589  nmcexi  29599  riesz4i  29636  mdi  29868  mdbr3  29870  mdbr4  29871  dmdi  29875  dmdbr3  29878  dmdbr4  29879  dmdi4  29880  mdslmd1i  29902  atss  29919  atom1d  29926  atmd  29972  sumdmdlem2  29992  cdj1i  30006  cdj3i  30014  fnpreimac  30195  nn0min  30307  archiabllem1a  30518  archiabllem2a  30521  archiabl  30525  isarchiofld  30601  crefi  30787  pcmplfin  30800  fmcncfil  30850  sigaclcu  31053  unelsiga  31070  sigapildsys  31098  ldgenpisys  31102  measvun  31145  carsgclctunlem2  31254  sibfima  31273  derangenlem  32043  subfacp1lem5  32056  subfacp1lem6  32057  resconn  32118  cvmcov  32135  cvmliftlem3  32159  cvmliftphtlem  32189  mclsax  32376  dfon2lem6  32593  poseq  32656  soseq  32657  nolt02o  32760  noresle  32761  noprefixmo  32763  nosupbnd1lem1  32769  nosupbnd1lem4  32772  nosupbnd2lem1  32776  nosupbnd2  32777  nocvxminlem  32808  fwddifnp1  33187  opnrebl2  33230  nn0prpwlem  33231  nn0prpw  33232  neibastop2lem  33269  neibastop2  33270  filnetlem4  33290  bj-mooreset  33944  bj-ismoored0  33949  bj-ismoored  33950  dfgcd3  34087  fin2so  34360  poimirlem25  34398  poimirlem29  34402  poimir  34406  mbfresfi  34419  ftc1cnnclem  34446  seqpo  34504  incsequz  34505  mettrifi  34514  geomcau  34516  caushft  34518  sstotbnd2  34534  equivtotbnd  34538  totbndbnd  34549  ismtybndlem  34566  heibor1lem  34569  bfplem2  34583  opidonOLD  34612  exidu1  34616  rngoideu  34663  isdrngo2  34718  unichnidl  34791  lsat0cv  35654  lcvexchlem4  35658  lcvexchlem5  35659  eqlkr3  35722  lub0N  35810  glb0N  35814  cvrnbtwn  35892  ltrneq2  36769  trlval2  36784  lpolsatN  38109  lpolpolsatN  38110  hdmap14lem12  38500  incssnn0  38744  lnmlssfg  39117  unxpwdom3  39132  neik0pk1imk0  39801  fnchoice  40745  monoordxrv  41224  monoord2xrv  41226  limcrecl  41376  fourierdlem54  41911  fourierdlem103  41960  fourierdlem104  41961  euoreqb  42749  smonoord  42972  iccpartlt  42991  iccpartgt  42994  iccpartdisj  43004  paireqne  43076  fmtnodvds  43109  perfectALTVlem2  43290  sbgoldbwt  43345  sbgoldbst  43346  sgoldbeven3prm  43351  mogoldbb  43353  nnsum4primesodd  43364  nnsum4primesoddALTV  43365  bgoldbnnsum3prm  43372  bgoldbtbndlem2  43374  bgoldbtbndlem3  43375  bgoldbtbndlem4  43376  bgoldbtbnd  43377  tgblthelfgott  43383  tgoldbach  43385  isomuspgrlem2c  43398  isomuspgrlem2d  43399  lcosslsp  43895  linindslinci  43905  lindslinindsimp1  43914  ldepsnlinclem1  43962  ldepsnlinclem2  43963