Theorem rspcv 3608

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2137, ax-11 2154, ax-12 2171. (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 482	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
4	1, 3	rspcdv 3604	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062

This theorem is referenced by:  rspccv  3609  rspcva  3610  rspccva  3611  rspcdva  3613  rspc2v  3621  rspc3v  3626  rspc4v  3629  rr19.3v  3656  rr19.28v  3657  rspsbc  3872  rspc2vd  3943  intmin  4971  ralxfrALT  5412  somo  5624  fr2nr  5653  weniso  7347  fr3nr  7755  limuni3  7837  tfinds  7845  funcnvuni  7918  poseq  8140  soseq  8141  suppfnss  8170  onnseq  8340  smo11  8360  tfrlem9  8381  tz7.49  8441  omeulem1  8578  oeordi  8583  naddelim  8681  nneneq  9205  nneneqOLD  9217  frfi  9284  unblem2  9292  unbnn2  9296  xpfiOLD  9314  ordiso2  9506  cantnflem1  9680  ttrcltr  9707  ttrclss  9711  ttrclselem2  9717  frins3  9746  rankunb  9841  tcrank  9875  carduni  9972  dfac8alem  10020  alephinit  10086  aceq3lem  10111  dfac5  10119  dfac12r  10137  dfac12k  10138  pwsdompw  10195  cflm  10241  isf32lem1  10344  isf32lem2  10345  isf34lem4  10368  hsmexlem4  10420  axcc3  10429  domtriomlem  10433  axdc3lem2  10442  axdc4lem  10446  axcclem  10448  axdclem  10510  alephval2  10563  winainflem  10684  eltskm  10834  squeeze0  12113  lbreu  12160  nnsub  12252  ublbneg  12913  zmax  12925  zbtwnre  12926  xrub  13287  infmremnf  13318  infmrp1  13319  fzrevral  13582  axdc4uzlem  13944  faclbnd4lem4  14252  ccatalpha  14539  wrdind  14668  wrd2ind  14669  reuccatpfxs1lem  14692  recan  15279  cau3lem  15297  caubnd2  15300  climrlim2  15487  climshftlem  15514  rlimcld2  15518  subcn2  15535  isercoll  15610  climcau  15613  serf0  15623  iseralt  15627  isumrpcl  15785  clim2prod  15830  ntrivcvgfvn0  15841  sqrt2irr  16188  ndvdssub  16348  dfgcd2  16484  lcmf  16566  lcmfunsnlem1  16570  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  lcmfdvdsb  16576  coprmgcdb  16582  coprmdvds1  16585  coprmprod  16594  coprmproddvdslem  16595  nprm  16621  dvdsprm  16636  coprm  16644  pcmpt  16821  pcmptdvds  16823  pcfac  16828  prmpwdvds  16833  unbenlem  16837  vdwlem10  16919  vdwlem13  16922  vdwnnlem1  16924  prmdvdsprmop  16972  prmgaplem7  16986  catideu  17615  initoid  17947  termoid  17948  initoeu1  17957  termoeu1  17964  isdrs2  18255  lublecllem  18309  lubun  18464  lidrididd  18585  sgrp2rid2ex  18804  dfgrp2  18843  grpidinv2  18878  dfgrp3lem  18917  issubg4  19019  efgi  19581  efgi2  19587  dprdss  19893  srgrz  20023  srglz  20024  srgisid  20025  f1rhm0to0ALT  20272  islmodd  20469  rmodislmod  20532  rmodislmodOLD  20533  islmhm2  20641  rrgeq0i  20897  isdomn4  20910  ip2eq  21197  mvrf1  21536  cply1mul  21809  isclo2  22583  cnpnei  22759  cncls  22769  lmss  22793  cnt0  22841  isnrm2  22853  isreg2  22872  tgcmp  22896  uncmp  22898  dfconn2  22914  1stcclb  22939  2ndcctbss  22950  comppfsc  23027  kgencn2  23052  ptpjpre1  23066  txlm  23143  kqfvima  23225  kqt0lem  23231  isr0  23232  nrmr0reg  23244  fgss2  23369  isufil2  23403  cfinufil  23423  flimopn  23470  fbflim2  23472  flfneii  23487  cnpflf  23496  fclssscls  23513  fclsnei  23514  fclsrest  23519  flimfnfcls  23523  fclscmp  23525  isfcf  23529  fcfnei  23530  alexsubALTlem3  23544  alexsubALTlem4  23545  alexsubALT  23546  tsmsgsum  23634  tsmsres  23639  tsmsxplem1  23648  ustincl  23703  ustdiag  23704  ustinvel  23705  ustexhalf  23706  cfiluexsm  23786  psmet0  23805  prdsbl  23991  metss  24008  metcnp3  24040  isngp4  24112  nmoi  24236  mulc1cncf  24412  cncfco  24414  lebnumii  24473  iscfil3  24781  iscau2  24785  iscau4  24787  equivcfil  24807  equivcau  24808  lmcau  24821  ismbf  25136  ellimc3  25387  lhop1  25522  dvfsumlem4  25537  dvfsum2  25542  dgrco  25780  fta1  25812  aalioulem2  25837  aalioulem4  25839  ulmclm  25890  ulmshftlem  25892  ulmcaulem  25897  ulmcau  25898  ulmcn  25902  cxploglim  26471  ftalem3  26568  chtub  26704  dchrelbasd  26731  2sqlem6  26915  2sqlem10  26920  dchrisumlema  26980  dchrisumlem2  26982  dchrisumlem3  26983  dchrvmasumlem2  26990  pntpbnd1  27078  pntibnd  27085  pntleml  27103  nolt02o  27187  noresle  27189  nosupbnd1lem1  27200  nosupbnd1lem4  27203  nosupbnd2lem1  27207  nosupbnd2  27208  nocvxminlem  27268  madebdaylemold  27381  brbtwn2  28152  colinearalg  28157  axcontlem4  28214  usgruspgrb  28430  cusgredg  28670  cusgrres  28694  usgredgsscusgredg  28705  fusgrn0degnn0  28745  wlk1walk  28885  wlkres  28916  wlkp1lem6  28924  wlkdlem2  28929  upgrwlkdvdelem  28982  pthdlem2lem  29013  lfgrn1cycl  29048  wwlksnredwwlkn  29138  wwlksnextproplem2  29153  clwwlkccatlem  29231  clwlkclwwlkf1lem3  29248  clwwisshclwwslemlem  29255  clwwlkf1  29291  clwwlkext2edg  29298  3cyclfrgrrn1  29527  n4cyclfrgr  29533  frgrwopregasn  29558  frgrwopregbsn  29559  isgrpo  29737  blocnilem  30044  ip2eqi  30096  htthlem  30157  hial0  30342  hial02  30343  hial2eq  30346  ocorth  30531  h1de2i  30793  pjjsi  30940  lnopunilem1  31250  lnophmlem1  31256  nmcexi  31266  riesz4i  31303  mdi  31535  mdbr3  31537  mdbr4  31538  dmdi  31542  dmdbr3  31545  dmdbr4  31546  dmdi4  31547  mdslmd1i  31569  atss  31586  atom1d  31593  atmd  31639  sumdmdlem2  31659  cdj1i  31673  cdj3i  31681  fnpreimac  31883  nn0min  32013  archiabllem1a  32324  archiabllem2a  32327  archiabl  32331  isarchiofld  32423  crefi  32815  pcmplfin  32828  fmcncfil  32899  sigaclcu  33103  unelsiga  33120  sigapildsys  33148  ldgenpisys  33152  measvun  33195  carsgclctunlem2  33306  sibfima  33325  fnrelpredd  34080  pfxwlk  34102  derangenlem  34150  subfacp1lem6  34164  resconn  34225  cvmcov  34242  cvmliftlem3  34266  cvmliftphtlem  34296  satfdmfmla  34379  mclsax  34548  dfon2lem6  34748  fwddifnp1  35125  opnrebl2  35194  nn0prpwlem  35195  nn0prpw  35196  neibastop2lem  35233  neibastop2  35234  filnetlem4  35254  bj-mooreset  35971  bj-ismoored0  35975  dfgcd3  36193  fin2so  36463  poimirlem25  36501  poimirlem29  36505  poimir  36509  mbfresfi  36522  ftc1cnnclem  36547  seqpo  36603  incsequz  36604  mettrifi  36613  geomcau  36615  caushft  36617  sstotbnd2  36630  equivtotbnd  36634  totbndbnd  36645  ismtybndlem  36662  heibor1lem  36665  bfplem2  36679  opidonOLD  36708  exidu1  36712  rngoideu  36759  isdrngo2  36814  unichnidl  36887  lsat0cv  37891  lcvexchlem4  37895  lcvexchlem5  37896  eqlkr3  37959  lub0N  38047  glb0N  38051  cvrnbtwn  38129  ltrneq2  39007  trlval2  39022  lpolsatN  40347  lpolpolsatN  40348  hdmap14lem12  40738  fsuppind  41159  nna4b4nsq  41398  incssnn0  41434  lnmlssfg  41807  unxpwdom3  41822  neik0pk1imk0  42783  ismnushort  43045  fnchoice  43698  monoordxrv  44178  monoord2xrv  44180  limcrecl  44331  fourierdlem54  44862  fourierdlem103  44911  fourierdlem104  44912  euoreqb  45803  smonoord  46025  iccpartlt  46078  iccpartgt  46081  iccpartdisj  46091  paireqne  46165  fmtnodvds  46198  perfectALTVlem2  46376  sbgoldbwt  46431  sbgoldbst  46432  sgoldbeven3prm  46437  mogoldbb  46439  nnsum4primesodd  46450  nnsum4primesoddALTV  46451  bgoldbnnsum3prm  46458  bgoldbtbndlem2  46460  bgoldbtbndlem3  46461  bgoldbtbndlem4  46462  bgoldbtbnd  46463  tgblthelfgott  46469  tgoldbach  46471  isomuspgrlem2c  46484  isomuspgrlem2d  46485  rnglidlmcl  46732  lcosslsp  47072  linindslinci  47082  lindslinindsimp1  47091  ldepsnlinclem1  47139  ldepsnlinclem2  47140  iscnrm3r  47534