Theorem rspcv 3587

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2142, ax-11 2158, ax-12 2178. (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 3583	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  rspccv  3588  rspcva  3589  rspccva  3590  rspcdva  3592  rspc2v  3602  rspc3v  3607  rspc4v  3611  rr19.3v  3636  rr19.28v  3637  rspsbc  3845  rspc2vd  3913  intmin  4935  ralxfrALT  5373  somo  5588  fr2nr  5618  weniso  7332  fr3nr  7751  limuni3  7831  tfinds  7839  funcnvuni  7911  resf1extb  7913  poseq  8140  soseq  8141  suppfnss  8171  onnseq  8316  smo11  8336  tfrlem9  8356  tz7.49  8416  omeulem1  8549  oeordi  8554  naddelim  8653  nneneq  9176  frfi  9239  unblem2  9247  unbnn2  9251  xpfiOLD  9277  ordiso2  9475  cantnflem1  9649  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  frins3  9715  rankunb  9810  tcrank  9844  carduni  9941  dfac8alem  9989  alephinit  10055  aceq3lem  10080  dfac5  10089  dfac12r  10107  dfac12k  10108  pwsdompw  10163  cflm  10210  isf32lem1  10313  isf32lem2  10314  isf34lem4  10337  hsmexlem4  10389  axcc3  10398  domtriomlem  10402  axdc3lem2  10411  axdc4lem  10415  axcclem  10417  axdclem  10479  alephval2  10532  winainflem  10653  eltskm  10803  squeeze0  12093  lbreu  12140  nnsub  12237  ublbneg  12899  zmax  12911  zbtwnre  12912  xrub  13279  infmremnf  13311  infmrp1  13312  fzrevral  13580  axdc4uzlem  13955  faclbnd4lem4  14268  ccatalpha  14565  wrdind  14694  wrd2ind  14695  reuccatpfxs1lem  14718  recan  15310  cau3lem  15328  caubnd2  15331  climrlim2  15520  climshftlem  15547  rlimcld2  15551  subcn2  15568  isercoll  15641  climcau  15644  serf0  15654  iseralt  15658  isumrpcl  15816  clim2prod  15861  ntrivcvgfvn0  15872  sqrt2irr  16224  ndvdssub  16386  dfgcd2  16523  lcmf  16610  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfdvdsb  16620  coprmgcdb  16626  coprmdvds1  16629  coprmprod  16638  coprmproddvdslem  16639  nprm  16665  dvdsprm  16680  coprm  16688  pcmpt  16870  pcmptdvds  16872  pcfac  16877  prmpwdvds  16882  unbenlem  16886  vdwlem10  16968  vdwlem13  16971  vdwnnlem1  16973  prmdvdsprmop  17021  prmgaplem7  17035  catideu  17643  initoid  17970  termoid  17971  initoeu1  17980  termoeu1  17987  isdrs2  18274  lublecllem  18326  lubun  18481  lidrididd  18604  sgrp2rid2ex  18861  dfgrp2  18901  grpidinv2  18936  dfgrp3lem  18977  issubg4  19084  efgi  19656  efgi2  19662  dprdss  19968  srgrz  20123  srglz  20124  srgisid  20125  rrgeq0i  20615  isdomn4  20632  islmodd  20779  rmodislmod  20843  islmhm2  20952  rnglidlmcl  21133  ip2eq  21569  mvrf1  21902  psdmul  22060  cply1mul  22190  isclo2  22982  cnpnei  23158  cncls  23168  lmss  23192  cnt0  23240  isnrm2  23252  isreg2  23271  tgcmp  23295  uncmp  23297  dfconn2  23313  1stcclb  23338  2ndcctbss  23349  comppfsc  23426  kgencn2  23451  ptpjpre1  23465  txlm  23542  kqfvima  23624  kqt0lem  23630  isr0  23631  nrmr0reg  23643  fgss2  23768  isufil2  23802  cfinufil  23822  flimopn  23869  fbflim2  23871  flfneii  23886  cnpflf  23895  fclssscls  23912  fclsnei  23913  fclsrest  23918  flimfnfcls  23922  fclscmp  23924  isfcf  23928  fcfnei  23929  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  tsmsgsum  24033  tsmsres  24038  tsmsxplem1  24047  ustincl  24102  ustdiag  24103  ustinvel  24104  ustexhalf  24105  cfiluexsm  24184  psmet0  24203  prdsbl  24386  metss  24403  metcnp3  24435  isngp4  24507  nmoi  24623  mulc1cncf  24805  cncfco  24807  lebnumii  24872  iscfil3  25180  iscau2  25184  iscau4  25186  equivcfil  25206  equivcau  25207  lmcau  25220  ismbf  25536  ellimc3  25787  lhop1  25926  dvfsumlem4  25943  dvfsum2  25948  dgrco  26188  fta1  26223  aalioulem2  26248  aalioulem4  26250  ulmclm  26303  ulmshftlem  26305  ulmcaulem  26310  ulmcau  26311  ulmcn  26315  cxploglim  26895  ftalem3  26992  chtub  27130  dchrelbasd  27157  2sqlem6  27341  2sqlem10  27346  dchrisumlema  27406  dchrisumlem2  27408  dchrisumlem3  27409  dchrvmasumlem2  27416  pntpbnd1  27504  pntibnd  27511  pntleml  27529  nolt02o  27614  noresle  27616  nosupbnd1lem1  27627  nosupbnd1lem4  27630  nosupbnd2lem1  27634  nosupbnd2  27635  nocvxminlem  27696  madebdaylemold  27816  n0subs  28260  brbtwn2  28839  colinearalg  28844  axcontlem4  28901  usgruspgrb  29117  cusgredg  29358  cusgrres  29383  usgredgsscusgredg  29394  fusgrn0degnn0  29434  wlk1walk  29574  wlkres  29605  wlkp1lem6  29613  wlkdlem2  29618  upgrwlkdvdelem  29673  pthdlem2lem  29704  lfgrn1cycl  29742  wwlksnredwwlkn  29832  wwlksnextproplem2  29847  clwwlkccatlem  29925  clwlkclwwlkf1lem3  29942  clwwisshclwwslemlem  29949  clwwlkf1  29985  clwwlkext2edg  29992  3cyclfrgrrn1  30221  n4cyclfrgr  30227  frgrwopregasn  30252  frgrwopregbsn  30253  isgrpo  30433  blocnilem  30740  ip2eqi  30792  htthlem  30853  hial0  31038  hial02  31039  hial2eq  31042  ocorth  31227  h1de2i  31489  pjjsi  31636  lnopunilem1  31946  lnophmlem1  31952  nmcexi  31962  riesz4i  31999  mdi  32231  mdbr3  32233  mdbr4  32234  dmdi  32238  dmdbr3  32241  dmdbr4  32242  dmdi4  32243  mdslmd1i  32265  atss  32282  atom1d  32289  atmd  32335  sumdmdlem2  32355  cdj1i  32369  cdj3i  32377  fnpreimac  32602  nn0min  32752  archiabllem1a  33152  archiabllem2a  33155  archiabl  33159  isarchiofld  33302  trisecnconstr  33789  crefi  33844  pcmplfin  33857  fmcncfil  33928  sigaclcu  34114  unelsiga  34131  sigapildsys  34159  ldgenpisys  34163  measvun  34206  carsgclctunlem2  34317  sibfima  34336  fnrelpredd  35086  pfxwlk  35118  derangenlem  35165  subfacp1lem6  35179  resconn  35240  cvmcov  35257  cvmliftlem3  35281  cvmliftphtlem  35311  satfdmfmla  35394  mclsax  35563  dfon2lem6  35783  fwddifnp1  36160  opnrebl2  36316  nn0prpwlem  36317  nn0prpw  36318  neibastop2lem  36355  neibastop2  36356  filnetlem4  36376  bj-mooreset  37097  bj-ismoored0  37101  dfgcd3  37319  fin2so  37608  poimirlem25  37646  poimirlem29  37650  poimir  37654  mbfresfi  37667  ftc1cnnclem  37692  seqpo  37748  incsequz  37749  mettrifi  37758  geomcau  37760  caushft  37762  sstotbnd2  37775  equivtotbnd  37779  totbndbnd  37790  ismtybndlem  37807  heibor1lem  37810  bfplem2  37824  opidonOLD  37853  exidu1  37857  rngoideu  37904  isdrngo2  37959  unichnidl  38032  lsat0cv  39033  lcvexchlem4  39037  lcvexchlem5  39038  eqlkr3  39101  lub0N  39189  glb0N  39193  cvrnbtwn  39271  ltrneq2  40149  trlval2  40164  lpolsatN  41489  lpolpolsatN  41490  hdmap14lem12  41880  fsuppind  42585  nna4b4nsq  42655  incssnn0  42706  lnmlssfg  43076  unxpwdom3  43091  neik0pk1imk0  44043  ismnushort  44297  fnchoice  45030  monoordxrv  45484  monoord2xrv  45486  limcrecl  45634  fourierdlem54  46165  fourierdlem103  46214  fourierdlem104  46215  euoreqb  47114  smonoord  47376  iccpartlt  47429  iccpartgt  47432  iccpartdisj  47442  paireqne  47516  fmtnodvds  47549  perfectALTVlem2  47727  sbgoldbwt  47782  sbgoldbst  47783  sgoldbeven3prm  47788  mogoldbb  47790  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  bgoldbnnsum3prm  47809  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbndlem4  47813  bgoldbtbnd  47814  tgblthelfgott  47820  tgoldbach  47822  grimuhgr  47891  grimcnv  47892  grimco  47893  uhgrimedgi  47894  isuspgrim0  47898  upgrimwlklem5  47905  uhgrimisgrgriclem  47934  clnbgrgrimlem  47937  clnbgrgrim  47938  grimedg  47939  uspgrlimlem3  47993  uspgrlimlem4  47994  grlimgrtrilem2  47998  grlimgrtri  47999  grilcbri2  48007  grlicsym  48009  grlictr  48011  clnbgr3stgrgrlic  48015  lcosslsp  48431  linindslinci  48441  lindslinindsimp1  48450  ldepsnlinclem1  48498  ldepsnlinclem2  48499  iscnrm3r  48940  initc  49084  termc2  49511