Theorem rspcv 3568

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2144, ax-11 2160, ax-12 2180. (Revised by SN, 12-Dec-2023.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcv	⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcv

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3564	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048

This theorem is referenced by:  rspccv  3569  rspcva  3570  rspccva  3571  rspcdva  3573  rspc2v  3583  rspc3v  3588  rspc4v  3592  rr19.3v  3617  rr19.28v  3618  rspsbc  3825  rspc2vd  3893  intmin  4913  ralxfrALT  5348  somo  5558  fr2nr  5588  weniso  7283  fr3nr  7700  limuni3  7777  tfinds  7785  funcnvuni  7857  resf1extb  7859  poseq  8083  soseq  8084  suppfnss  8114  onnseq  8259  smo11  8279  tfrlem9  8299  tz7.49  8359  omeulem1  8492  oeordi  8497  naddelim  8596  nneneq  9110  frfi  9164  unblem2  9172  unbnn2  9176  ordiso2  9396  cantnflem1  9574  ttrcltr  9601  ttrclss  9605  ttrclselem2  9611  frins3  9643  rankunb  9738  tcrank  9772  carduni  9869  dfac8alem  9915  alephinit  9981  aceq3lem  10006  dfac5  10015  dfac12r  10033  dfac12k  10034  pwsdompw  10089  cflm  10136  isf32lem1  10239  isf32lem2  10240  isf34lem4  10263  hsmexlem4  10315  axcc3  10324  domtriomlem  10328  axdc3lem2  10337  axdc4lem  10341  axcclem  10343  axdclem  10405  alephval2  10458  winainflem  10579  eltskm  10729  squeeze0  12020  lbreu  12067  nnsub  12164  ublbneg  12826  zmax  12838  zbtwnre  12839  xrub  13206  infmremnf  13238  infmrp1  13239  fzrevral  13507  axdc4uzlem  13885  faclbnd4lem4  14198  ccatalpha  14496  wrdind  14624  wrd2ind  14625  reuccatpfxs1lem  14648  recan  15239  cau3lem  15257  caubnd2  15260  climrlim2  15449  climshftlem  15476  rlimcld2  15480  subcn2  15497  isercoll  15570  climcau  15573  serf0  15583  iseralt  15587  isumrpcl  15745  clim2prod  15790  ntrivcvgfvn0  15801  sqrt2irr  16153  ndvdssub  16315  dfgcd2  16452  lcmf  16539  lcmfunsnlem1  16543  lcmfunsnlem2lem1  16544  lcmfunsnlem2lem2  16545  lcmfdvdsb  16549  coprmgcdb  16555  coprmdvds1  16558  coprmprod  16567  coprmproddvdslem  16568  nprm  16594  dvdsprm  16609  coprm  16617  pcmpt  16799  pcmptdvds  16801  pcfac  16806  prmpwdvds  16811  unbenlem  16815  vdwlem10  16897  vdwlem13  16900  vdwnnlem1  16902  prmdvdsprmop  16950  prmgaplem7  16964  catideu  17576  initoid  17903  termoid  17904  initoeu1  17913  termoeu1  17920  isdrs2  18207  lublecllem  18259  lubun  18416  lidrididd  18573  sgrp2rid2ex  18830  dfgrp2  18870  grpidinv2  18905  dfgrp3lem  18946  issubg4  19053  efgi  19626  efgi2  19632  dprdss  19938  srgrz  20120  srglz  20121  srgisid  20122  rrgeq0i  20609  isdomn4  20626  islmodd  20794  rmodislmod  20858  islmhm2  20967  rnglidlmcl  21148  ip2eq  21585  mvrf1  21918  psdmul  22076  cply1mul  22206  isclo2  22998  cnpnei  23174  cncls  23184  lmss  23208  cnt0  23256  isnrm2  23268  isreg2  23287  tgcmp  23311  uncmp  23313  dfconn2  23329  1stcclb  23354  2ndcctbss  23365  comppfsc  23442  kgencn2  23467  ptpjpre1  23481  txlm  23558  kqfvima  23640  kqt0lem  23646  isr0  23647  nrmr0reg  23659  fgss2  23784  isufil2  23818  cfinufil  23838  flimopn  23885  fbflim2  23887  flfneii  23902  cnpflf  23911  fclssscls  23928  fclsnei  23929  fclsrest  23934  flimfnfcls  23938  fclscmp  23940  isfcf  23944  fcfnei  23945  alexsubALTlem3  23959  alexsubALTlem4  23960  alexsubALT  23961  tsmsgsum  24049  tsmsres  24054  tsmsxplem1  24063  ustincl  24118  ustdiag  24119  ustinvel  24120  ustexhalf  24121  cfiluexsm  24199  psmet0  24218  prdsbl  24401  metss  24418  metcnp3  24450  isngp4  24522  nmoi  24638  mulc1cncf  24820  cncfco  24822  lebnumii  24887  iscfil3  25195  iscau2  25199  iscau4  25201  equivcfil  25221  equivcau  25222  lmcau  25235  ismbf  25551  ellimc3  25802  lhop1  25941  dvfsumlem4  25958  dvfsum2  25963  dgrco  26203  fta1  26238  aalioulem2  26263  aalioulem4  26265  ulmclm  26318  ulmshftlem  26320  ulmcaulem  26325  ulmcau  26326  ulmcn  26330  cxploglim  26910  ftalem3  27007  chtub  27145  dchrelbasd  27172  2sqlem6  27356  2sqlem10  27361  dchrisumlema  27421  dchrisumlem2  27423  dchrisumlem3  27424  dchrvmasumlem2  27431  pntpbnd1  27519  pntibnd  27526  pntleml  27544  nolt02o  27629  noresle  27631  nosupbnd1lem1  27642  nosupbnd1lem4  27645  nosupbnd2lem1  27649  nosupbnd2  27650  nocvxminlem  27712  madebdaylemold  27838  n0subs  28284  zs12zodd  28387  brbtwn2  28878  colinearalg  28883  axcontlem4  28940  usgruspgrb  29156  cusgredg  29397  cusgrres  29422  usgredgsscusgredg  29433  fusgrn0degnn0  29473  wlk1walk  29612  wlkres  29642  wlkp1lem6  29650  wlkdlem2  29655  upgrwlkdvdelem  29709  pthdlem2lem  29740  lfgrn1cycl  29778  wwlksnredwwlkn  29868  wwlksnextproplem2  29883  clwwlkccatlem  29961  clwlkclwwlkf1lem3  29978  clwwisshclwwslemlem  29985  clwwlkf1  30021  clwwlkext2edg  30028  3cyclfrgrrn1  30257  n4cyclfrgr  30263  frgrwopregasn  30288  frgrwopregbsn  30289  isgrpo  30469  blocnilem  30776  ip2eqi  30828  htthlem  30889  hial0  31074  hial02  31075  hial2eq  31078  ocorth  31263  h1de2i  31525  pjjsi  31672  lnopunilem1  31982  lnophmlem1  31988  nmcexi  31998  riesz4i  32035  mdi  32267  mdbr3  32269  mdbr4  32270  dmdi  32274  dmdbr3  32277  dmdbr4  32278  dmdi4  32279  mdslmd1i  32301  atss  32318  atom1d  32325  atmd  32371  sumdmdlem2  32391  cdj1i  32405  cdj3i  32413  fnpreimac  32645  nn0min  32795  archiabllem1a  33152  archiabllem2a  33155  archiabl  33159  isarchiofld  33160  trisecnconstr  33797  crefi  33852  pcmplfin  33865  fmcncfil  33936  sigaclcu  34122  unelsiga  34139  sigapildsys  34167  ldgenpisys  34171  measvun  34214  carsgclctunlem2  34324  sibfima  34343  fnrelpredd  35094  fineqvnttrclse  35136  pfxwlk  35160  derangenlem  35207  subfacp1lem6  35221  resconn  35282  cvmcov  35299  cvmliftlem3  35323  cvmliftphtlem  35353  satfdmfmla  35436  mclsax  35605  dfon2lem6  35822  fwddifnp1  36199  opnrebl2  36355  nn0prpwlem  36356  nn0prpw  36357  neibastop2lem  36394  neibastop2  36395  filnetlem4  36415  bj-mooreset  37136  bj-ismoored0  37140  dfgcd3  37358  fin2so  37647  poimirlem25  37685  poimirlem29  37689  poimir  37693  mbfresfi  37706  ftc1cnnclem  37731  seqpo  37787  incsequz  37788  mettrifi  37797  geomcau  37799  caushft  37801  sstotbnd2  37814  equivtotbnd  37818  totbndbnd  37829  ismtybndlem  37846  heibor1lem  37849  bfplem2  37863  opidonOLD  37892  exidu1  37896  rngoideu  37943  isdrngo2  37998  unichnidl  38071  lsat0cv  39072  lcvexchlem4  39076  lcvexchlem5  39077  eqlkr3  39140  lub0N  39228  glb0N  39232  cvrnbtwn  39310  ltrneq2  40187  trlval2  40202  lpolsatN  41527  lpolpolsatN  41528  hdmap14lem12  41918  fsuppind  42623  nna4b4nsq  42693  incssnn0  42744  lnmlssfg  43113  unxpwdom3  43128  neik0pk1imk0  44080  ismnushort  44334  fnchoice  45066  monoordxrv  45519  monoord2xrv  45521  limcrecl  45669  fourierdlem54  46198  fourierdlem103  46247  fourierdlem104  46248  euoreqb  47140  smonoord  47402  iccpartlt  47455  iccpartgt  47458  iccpartdisj  47468  paireqne  47542  fmtnodvds  47575  perfectALTVlem2  47753  sbgoldbwt  47808  sbgoldbst  47809  sgoldbeven3prm  47814  mogoldbb  47816  nnsum4primesodd  47827  nnsum4primesoddALTV  47828  bgoldbnnsum3prm  47835  bgoldbtbndlem2  47837  bgoldbtbndlem3  47838  bgoldbtbndlem4  47839  bgoldbtbnd  47840  tgblthelfgott  47846  tgoldbach  47848  grimuhgr  47918  grimcnv  47919  grimco  47920  uhgrimedgi  47921  isuspgrim0  47925  upgrimwlklem5  47932  uhgrimisgrgriclem  47961  clnbgrgrimlem  47964  clnbgrgrim  47965  grimedg  47966  uspgrlimlem3  48021  uspgrlimlem4  48022  grlimedgclnbgr  48026  grlimgrtrilem2  48033  grlimgrtri  48034  grilcbri2  48042  grlicsym  48044  grlictr  48046  clnbgr3stgrgrlim  48050  clnbgr3stgrgrlic  48051  lcosslsp  48470  linindslinci  48480  lindslinindsimp1  48489  ldepsnlinclem1  48537  ldepsnlinclem2  48538  iscnrm3r  48979  initc  49123  termc2  49550