Theorem rspcv 3572

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2177, ax-11 2193, ax-12 2212. (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 23	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵)
2		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	adantl 487	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3568	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rspccv  3573  rspcva  3574  rspccva  3575  rspcdva  3577  rspc2v  3586  rspc3v  3591  rspc4v  3595  rr19.3v  3620  rr19.28v  3621  rspsbc  3826  rspc2vd  3895  intmin  4927  ralxfrALT  5377  somo  5598  fr2nr  5628  weniso  7368  fr3nr  7790  limuni3  7867  tfinds  7875  funcnvuni  7948  resf1extb  7950  poseq  8181  soseq  8182  suppfnss  8213  onnseq  8359  smo11  8379  tfrlem9  8400  tz7.49  8462  omeulem1  8597  oeordi  8603  naddelim  8703  nneneq  9228  frfi  9283  unblem2  9292  unbnn2  9296  ordiso2  9516  cantnflem1  9697  ttrcltr  9724  ttrclss  9728  ttrclselem2  9734  frins3  9766  rankunb  9871  tcrank  9908  scottex  9940  carduni  10069  dfac8alem  10115  alephinit  10181  aceq3lem  10206  dfac5  10214  dfac12r  10232  dfac12k  10233  pwsdompw  10288  cflm  10334  isf32lem1  10438  isf32lem2  10439  isf34lem4  10462  hsmexlem4  10514  axcc3  10523  domtriomlem  10527  axdc3lem2  10536  axdc4lem  10540  axcclem  10542  axdclem  10604  alephval2  10664  winainflem  10785  eltskm  10935  squeeze0  12227  lbreu  12274  nnsub  12389  ublbneg  13067  zmax  13079  zbtwnre  13080  xrub  13449  infmremnf  13481  infmrp1  13482  fzrevral  13753  axdc4uzlem  14133  faclbnd4lem4  14447  ccatalpha  14747  wrdind  14879  wrd2ind  14880  reuccatpfxs1lem  14903  recan  15513  cau3lem  15531  caubnd2  15534  climrlim2  15723  climshftlem  15750  rlimcld2  15754  subcn2  15771  isercoll  15844  climcau  15847  serf0  15857  iseralt  15861  isumrpcl  16021  clim2prod  16066  ntrivcvgfvn0  16077  sqrt2irr  16426  ndvdssub  16588  dfgcd2  16728  lcmf  16817  lcmfunsnlem1  16821  lcmfunsnlem2lem1  16822  lcmfunsnlem2lem2  16823  lcmfdvdsb  16827  coprmgcdb  16833  coprmdvds1  16836  coprmprod  16845  coprmproddvdslem  16846  nprm  16872  dvdsprm  16888  coprm  16896  pcmpt  17079  pcmptdvds  17081  pcfac  17086  prmpwdvds  17091  unbenlem  17095  vdwlem10  17177  vdwlem13  17180  vdwnnlem1  17182  prmdvdsprmop  17230  prmgaplem7  17244  catideu  17858  initoid  18185  termoid  18186  initoeu1  18195  termoeu1  18202  isdrs2  18489  lublecllem  18541  lubun  18698  lidrididd  18860  mgmidpfod  18866  sgrp2rid2ex  19135  dfgrp2  19182  grpidinv2  19217  dfgrp3lem  19257  issubg4  19365  efgi  19942  efgi2  19948  dprdss  20254  srgrz  20442  srglz  20443  srgisid  20444  rrgeq0i  20960  isdomn4  20976  isdrng3lem2  21015  islmodd  21150  rmodislmod  21214  islmhm2  21322  rnglidlmcl  21504  ip2eq  21968  mvrf1  22302  psdmul  22496  cply1mul  22623  isclo2  23415  cnpnei  23591  cncls  23601  lmss  23625  cnt0  23673  isnrm2  23685  isreg2  23704  tgcmp  23728  uncmp  23730  dfconn2  23746  1stcclb  23771  2ndcctbss  23783  comppfsc  23860  kgencn2  23885  ptpjpre1  23899  txlm  23976  kqfvima  24058  kqt0lem  24064  isr0  24065  nrmr0reg  24077  fgss2  24202  isufil2  24236  cfinufil  24256  flimopn  24303  fbflim2  24305  flfneii  24320  cnpflf  24329  fclssscls  24346  fclsnei  24347  fclsrest  24352  flimfnfcls  24356  fclscmp  24358  isfcf  24362  fcfnei  24363  alexsubALTlem3  24377  alexsubALTlem4  24378  alexsubALT  24379  tsmsgsum  24467  tsmsres  24472  tsmsxplem1  24481  ustincl  24536  ustdiag  24537  ustinvel  24538  ustexhalf  24539  cfiluexsm  24617  psmet0  24636  prdsbl  24819  metss  24836  metcnp3  24868  isngp4  24940  nmoi  25056  mulc1cncf  25235  cncfco  25237  lebnumii  25296  iscfil3  25603  iscau2  25607  iscau4  25609  equivcfil  25629  equivcau  25630  lmcau  25643  ismbf  25958  ellimc3  26208  lhop1  26343  dvfsumlem4  26358  dvfsum2  26363  dgrco  26603  fta1  26638  plyconz  26640  aalioulem2  26669  aalioulem4  26671  ulmclm  26723  ulmshftlem  26725  ulmcaulem  26730  ulmcau  26731  ulmcn  26735  cxploglim  27314  ftalem3  27411  chtub  27548  dchrelbasd  27575  2sqlem6  27759  2sqlem10  27764  dchrisumlema  27824  dchrisumlem2  27826  dchrisumlem3  27827  dchrvmasumlem2  27834  pntpbnd1  27922  pntibnd  27929  pntleml  27947  fltoprm  28004  nolt02o  28061  noresle  28063  nosupbnd1lem1  28074  nosupbnd1lem4  28077  nosupbnd2lem1  28081  nosupbnd2  28082  nocvxminlem  28149  madebdaylemold  28293  n0subs  28758  z12zsodd  28877  brbtwn2  29492  colinearalg  29497  axcontlem4  29554  usgruspgrb  29773  cusgredg  30014  cusgrres  30038  usgredgsscusgredg  30049  fusgrn0degnn0  30089  wlk1walk  30228  wlkres  30258  wlkp1lem6  30266  wlkdlem2  30271  pfxwlk  30275  upgrwlkdvdelem  30331  pthdlem2lem  30362  lfgrn1cycl  30403  wwlksnredwwlkn  30493  wwlksnextproplem2  30508  clwwlkccatlem  30589  clwlkclwwlkf1lem3  30606  clwwisshclwwslemlem  30613  clwwlkf1  30649  clwwlkext2edg  30656  3cyclfrgrrn1  30895  n4cyclfrgr  30901  frgrwopregasn  30926  frgrwopregbsn  30927  isgrpo  31108  blocnilem  31415  ip2eqi  31467  htthlem  31528  hial0  31713  hial02  31714  hial2eq  31717  ocorth  31902  h1de2i  32164  pjjsi  32311  lnopunilem1  32621  lnophmlem1  32627  nmcexi  32637  riesz4i  32674  mdi  32906  mdbr3  32908  mdbr4  32909  dmdi  32913  dmdbr3  32916  dmdbr4  32917  dmdi4  32918  mdslmd1i  32940  atss  32957  atom1d  32964  atmd  33010  sumdmdlem2  33030  cdj1i  33044  cdj3i  33052  fnpreimac  33315  nn0min  33462  archiabllem1a  33802  archiabllem2a  33805  archiabl  33809  isarchiofld  33810  trisecnconstr  34474  crefi  34529  pcmplfin  34542  fmcncfil  34613  sigaclcu  34799  unelsiga  34816  sigapildsys  34845  ldgenpisys  34849  measvun  34892  carsgclctunlem2  35001  sibfima  35020  fnrelpredd  35776  fineqvnttrclse  35852  fineqvinfep  35853  onprcf1acwevdlem2  35969  derangenlem  36026  subfacp1lem6  36040  resconn  36101  cvmcov  36118  cvmliftlem3  36142  cvmliftphtlem  36172  satfdmfmla  36255  mclsax  36424  mirimanoffr  36550  dfon2lem6  36646  fwddifnp1  37026  opnrebl2  37205  nn0prpwlem  37206  nn0prpw  37207  neibastop2lem  37244  neibastop2  37245  filnetlem4  37265  dfttc4  37414  bj-mooreset  38131  bj-ismoored0  38135  dfgcd3  38354  fin2so  38639  poimirlem25  38672  poimirlem29  38676  poimir  38680  mbfresfi  38693  ftc1cnnclem  38718  seqpo  38790  incsequz  38791  mettrifi  38800  geomcau  38802  caushft  38804  sstotbnd2  38817  equivtotbnd  38821  totbndbnd  38832  ismtybndlem  38849  heibor1lem  38852  bfplem2  38866  opidonOLD  38895  exidu1  38899  rngoideu  38946  isdrngo2  39001  unichnidl  39074  lsat0cv  40199  lcvexchlem4  40203  lcvexchlem5  40204  eqlkr3  40267  lub0N  40355  glb0N  40359  cvrnbtwn  40437  ltrneq2  41314  trlval2  41329  lpolsatN  42654  lpolpolsatN  42655  hdmap14lem12  43045  fsuppind  43727  incssnn0  43831  lnmlssfg  44191  unxpwdom3  44206  neik0pk1imk0  45156  ismnushort  45394  fnchoice  46154  monoordxrv  46599  monoord2xrv  46601  limcrecl  46749  fourierdlem54  47278  fourierdlem103  47327  fourierdlem104  47328  euoreqb  48288  smonoord  48555  iccpartlt  48614  iccpartgt  48617  iccpartdisj  48627  paireqne  48701  fmtnodvds  48737  perfectALTVlem2  48928  sbgoldbwt  48983  sbgoldbst  48984  sgoldbeven3prm  48989  mogoldbb  48991  nnsum4primesodd  49002  nnsum4primesoddALTV  49003  bgoldbnnsum3prm  49010  bgoldbtbndlem2  49012  bgoldbtbndlem3  49013  bgoldbtbndlem4  49014  bgoldbtbnd  49015  tgblthelfgott  49021  tgoldbach  49023  grimuhgr  49093  grimcnv  49094  grimco  49095  uhgrimedgi  49096  isuspgrim0  49100  upgrimwlklem5  49107  uhgrimisgrgriclem  49136  clnbgrgrimlem  49139  clnbgrgrim  49140  grimedg  49141  uspgrlimlem3  49196  uspgrlimlem4  49197  grlimedgclnbgr  49201  grlimgrtrilem2  49208  grlimgrtri  49209  grilcbri2  49217  grlicsym  49219  grlictr  49221  clnbgr3stgrgrlim  49225  clnbgr3stgrgrlic  49226  lcosslsp  49658  linindslinci  49668  lindslinindsimp1  49677  ldepsnlinclem1  49725  ldepsnlinclem2  49726  iscnrm3r  50170  initc  50314  termc2  50761  nellindf  51153