Theorem rspcv 3581

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 3577	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspccv  3582  rspcva  3583  rspccva  3584  rspcdva  3586  rspc2v  3596  rspc3v  3601  rspc4v  3605  rr19.3v  3630  rr19.28v  3631  rspsbc  3839  rspc2vd  3907  intmin  4928  ralxfrALT  5365  somo  5578  fr2nr  5608  weniso  7311  fr3nr  7728  limuni3  7808  tfinds  7816  funcnvuni  7888  resf1extb  7890  poseq  8114  soseq  8115  suppfnss  8145  onnseq  8290  smo11  8310  tfrlem9  8330  tz7.49  8390  omeulem1  8523  oeordi  8528  naddelim  8627  nneneq  9147  frfi  9208  unblem2  9216  unbnn2  9220  xpfiOLD  9246  ordiso2  9444  cantnflem1  9618  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  frins3  9684  rankunb  9779  tcrank  9813  carduni  9910  dfac8alem  9958  alephinit  10024  aceq3lem  10049  dfac5  10058  dfac12r  10076  dfac12k  10077  pwsdompw  10132  cflm  10179  isf32lem1  10282  isf32lem2  10283  isf34lem4  10306  hsmexlem4  10358  axcc3  10367  domtriomlem  10371  axdc3lem2  10380  axdc4lem  10384  axcclem  10386  axdclem  10448  alephval2  10501  winainflem  10622  eltskm  10772  squeeze0  12062  lbreu  12109  nnsub  12206  ublbneg  12868  zmax  12880  zbtwnre  12881  xrub  13248  infmremnf  13280  infmrp1  13281  fzrevral  13549  axdc4uzlem  13924  faclbnd4lem4  14237  ccatalpha  14534  wrdind  14663  wrd2ind  14664  reuccatpfxs1lem  14687  recan  15279  cau3lem  15297  caubnd2  15300  climrlim2  15489  climshftlem  15516  rlimcld2  15520  subcn2  15537  isercoll  15610  climcau  15613  serf0  15623  iseralt  15627  isumrpcl  15785  clim2prod  15830  ntrivcvgfvn0  15841  sqrt2irr  16193  ndvdssub  16355  dfgcd2  16492  lcmf  16579  lcmfunsnlem1  16583  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfdvdsb  16589  coprmgcdb  16595  coprmdvds1  16598  coprmprod  16607  coprmproddvdslem  16608  nprm  16634  dvdsprm  16649  coprm  16657  pcmpt  16839  pcmptdvds  16841  pcfac  16846  prmpwdvds  16851  unbenlem  16855  vdwlem10  16937  vdwlem13  16940  vdwnnlem1  16942  prmdvdsprmop  16990  prmgaplem7  17004  catideu  17612  initoid  17939  termoid  17940  initoeu1  17949  termoeu1  17956  isdrs2  18243  lublecllem  18295  lubun  18450  lidrididd  18573  sgrp2rid2ex  18830  dfgrp2  18870  grpidinv2  18905  dfgrp3lem  18946  issubg4  19053  efgi  19625  efgi2  19631  dprdss  19937  srgrz  20092  srglz  20093  srgisid  20094  rrgeq0i  20584  isdomn4  20601  islmodd  20748  rmodislmod  20812  islmhm2  20921  rnglidlmcl  21102  ip2eq  21538  mvrf1  21871  psdmul  22029  cply1mul  22159  isclo2  22951  cnpnei  23127  cncls  23137  lmss  23161  cnt0  23209  isnrm2  23221  isreg2  23240  tgcmp  23264  uncmp  23266  dfconn2  23282  1stcclb  23307  2ndcctbss  23318  comppfsc  23395  kgencn2  23420  ptpjpre1  23434  txlm  23511  kqfvima  23593  kqt0lem  23599  isr0  23600  nrmr0reg  23612  fgss2  23737  isufil2  23771  cfinufil  23791  flimopn  23838  fbflim2  23840  flfneii  23855  cnpflf  23864  fclssscls  23881  fclsnei  23882  fclsrest  23887  flimfnfcls  23891  fclscmp  23893  isfcf  23897  fcfnei  23898  alexsubALTlem3  23912  alexsubALTlem4  23913  alexsubALT  23914  tsmsgsum  24002  tsmsres  24007  tsmsxplem1  24016  ustincl  24071  ustdiag  24072  ustinvel  24073  ustexhalf  24074  cfiluexsm  24153  psmet0  24172  prdsbl  24355  metss  24372  metcnp3  24404  isngp4  24476  nmoi  24592  mulc1cncf  24774  cncfco  24776  lebnumii  24841  iscfil3  25149  iscau2  25153  iscau4  25155  equivcfil  25175  equivcau  25176  lmcau  25189  ismbf  25505  ellimc3  25756  lhop1  25895  dvfsumlem4  25912  dvfsum2  25917  dgrco  26157  fta1  26192  aalioulem2  26217  aalioulem4  26219  ulmclm  26272  ulmshftlem  26274  ulmcaulem  26279  ulmcau  26280  ulmcn  26284  cxploglim  26864  ftalem3  26961  chtub  27099  dchrelbasd  27126  2sqlem6  27310  2sqlem10  27315  dchrisumlema  27375  dchrisumlem2  27377  dchrisumlem3  27378  dchrvmasumlem2  27385  pntpbnd1  27473  pntibnd  27480  pntleml  27498  nolt02o  27583  noresle  27585  nosupbnd1lem1  27596  nosupbnd1lem4  27599  nosupbnd2lem1  27603  nosupbnd2  27604  nocvxminlem  27665  madebdaylemold  27785  n0subs  28229  brbtwn2  28808  colinearalg  28813  axcontlem4  28870  usgruspgrb  29086  cusgredg  29327  cusgrres  29352  usgredgsscusgredg  29363  fusgrn0degnn0  29403  wlk1walk  29542  wlkres  29572  wlkp1lem6  29580  wlkdlem2  29585  upgrwlkdvdelem  29639  pthdlem2lem  29670  lfgrn1cycl  29708  wwlksnredwwlkn  29798  wwlksnextproplem2  29813  clwwlkccatlem  29891  clwlkclwwlkf1lem3  29908  clwwisshclwwslemlem  29915  clwwlkf1  29951  clwwlkext2edg  29958  3cyclfrgrrn1  30187  n4cyclfrgr  30193  frgrwopregasn  30218  frgrwopregbsn  30219  isgrpo  30399  blocnilem  30706  ip2eqi  30758  htthlem  30819  hial0  31004  hial02  31005  hial2eq  31008  ocorth  31193  h1de2i  31455  pjjsi  31602  lnopunilem1  31912  lnophmlem1  31918  nmcexi  31928  riesz4i  31965  mdi  32197  mdbr3  32199  mdbr4  32200  dmdi  32204  dmdbr3  32207  dmdbr4  32208  dmdi4  32209  mdslmd1i  32231  atss  32248  atom1d  32255  atmd  32301  sumdmdlem2  32321  cdj1i  32335  cdj3i  32343  fnpreimac  32568  nn0min  32718  archiabllem1a  33118  archiabllem2a  33121  archiabl  33125  isarchiofld  33268  trisecnconstr  33755  crefi  33810  pcmplfin  33823  fmcncfil  33894  sigaclcu  34080  unelsiga  34097  sigapildsys  34125  ldgenpisys  34129  measvun  34172  carsgclctunlem2  34283  sibfima  34302  fnrelpredd  35052  pfxwlk  35084  derangenlem  35131  subfacp1lem6  35145  resconn  35206  cvmcov  35223  cvmliftlem3  35247  cvmliftphtlem  35277  satfdmfmla  35360  mclsax  35529  dfon2lem6  35749  fwddifnp1  36126  opnrebl2  36282  nn0prpwlem  36283  nn0prpw  36284  neibastop2lem  36321  neibastop2  36322  filnetlem4  36342  bj-mooreset  37063  bj-ismoored0  37067  dfgcd3  37285  fin2so  37574  poimirlem25  37612  poimirlem29  37616  poimir  37620  mbfresfi  37633  ftc1cnnclem  37658  seqpo  37714  incsequz  37715  mettrifi  37724  geomcau  37726  caushft  37728  sstotbnd2  37741  equivtotbnd  37745  totbndbnd  37756  ismtybndlem  37773  heibor1lem  37776  bfplem2  37790  opidonOLD  37819  exidu1  37823  rngoideu  37870  isdrngo2  37925  unichnidl  37998  lsat0cv  38999  lcvexchlem4  39003  lcvexchlem5  39004  eqlkr3  39067  lub0N  39155  glb0N  39159  cvrnbtwn  39237  ltrneq2  40115  trlval2  40130  lpolsatN  41455  lpolpolsatN  41456  hdmap14lem12  41846  fsuppind  42551  nna4b4nsq  42621  incssnn0  42672  lnmlssfg  43042  unxpwdom3  43057  neik0pk1imk0  44009  ismnushort  44263  fnchoice  44996  monoordxrv  45450  monoord2xrv  45452  limcrecl  45600  fourierdlem54  46131  fourierdlem103  46180  fourierdlem104  46181  euoreqb  47083  smonoord  47345  iccpartlt  47398  iccpartgt  47401  iccpartdisj  47411  paireqne  47485  fmtnodvds  47518  perfectALTVlem2  47696  sbgoldbwt  47751  sbgoldbst  47752  sgoldbeven3prm  47757  mogoldbb  47759  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  bgoldbnnsum3prm  47778  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  bgoldbtbndlem4  47782  bgoldbtbnd  47783  tgblthelfgott  47789  tgoldbach  47791  grimuhgr  47860  grimcnv  47861  grimco  47862  uhgrimedgi  47863  isuspgrim0  47867  upgrimwlklem5  47874  uhgrimisgrgriclem  47903  clnbgrgrimlem  47906  clnbgrgrim  47907  grimedg  47908  uspgrlimlem3  47962  uspgrlimlem4  47963  grlimgrtrilem2  47967  grlimgrtri  47968  grilcbri2  47976  grlicsym  47978  grlictr  47980  clnbgr3stgrgrlic  47984  lcosslsp  48400  linindslinci  48410  lindslinindsimp1  48419  ldepsnlinclem1  48467  ldepsnlinclem2  48468  iscnrm3r  48909  initc  49053  termc2  49480