Theorem rspcv 3561

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rspccv  3562  rspcva  3563  rspccva  3564  rspcdva  3566  rspc2v  3576  rspc3v  3581  rspc4v  3585  rr19.3v  3610  rr19.28v  3611  rspsbc  3818  rspc2vd  3886  intmin  4911  ralxfrALT  5352  somo  5571  fr2nr  5601  weniso  7302  fr3nr  7719  limuni3  7796  tfinds  7804  funcnvuni  7876  resf1extb  7878  poseq  8101  soseq  8102  suppfnss  8132  onnseq  8277  smo11  8297  tfrlem9  8317  tz7.49  8377  omeulem1  8510  oeordi  8516  naddelim  8615  nneneq  9133  frfi  9188  unblem2  9196  unbnn2  9200  ordiso2  9423  cantnflem1  9601  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  frins3  9670  rankunb  9765  tcrank  9799  carduni  9896  dfac8alem  9942  alephinit  10008  aceq3lem  10033  dfac5  10042  dfac12r  10060  dfac12k  10061  pwsdompw  10116  cflm  10163  isf32lem1  10266  isf32lem2  10267  isf34lem4  10290  hsmexlem4  10342  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc4lem  10368  axcclem  10370  axdclem  10432  alephval2  10486  winainflem  10607  eltskm  10757  squeeze0  12050  lbreu  12097  nnsub  12212  ublbneg  12874  zmax  12886  zbtwnre  12887  xrub  13255  infmremnf  13287  infmrp1  13288  fzrevral  13557  axdc4uzlem  13936  faclbnd4lem4  14249  ccatalpha  14547  wrdind  14675  wrd2ind  14676  reuccatpfxs1lem  14699  recan  15290  cau3lem  15308  caubnd2  15311  climrlim2  15500  climshftlem  15527  rlimcld2  15531  subcn2  15548  isercoll  15621  climcau  15624  serf0  15634  iseralt  15638  isumrpcl  15799  clim2prod  15844  ntrivcvgfvn0  15855  sqrt2irr  16207  ndvdssub  16369  dfgcd2  16506  lcmf  16593  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfdvdsb  16603  coprmgcdb  16609  coprmdvds1  16612  coprmprod  16621  coprmproddvdslem  16622  nprm  16648  dvdsprm  16664  coprm  16672  pcmpt  16854  pcmptdvds  16856  pcfac  16861  prmpwdvds  16866  unbenlem  16870  vdwlem10  16952  vdwlem13  16955  vdwnnlem1  16957  prmdvdsprmop  17005  prmgaplem7  17019  catideu  17632  initoid  17959  termoid  17960  initoeu1  17969  termoeu1  17976  isdrs2  18263  lublecllem  18315  lubun  18472  lidrididd  18629  sgrp2rid2ex  18889  dfgrp2  18929  grpidinv2  18964  dfgrp3lem  19005  issubg4  19112  efgi  19685  efgi2  19691  dprdss  19997  srgrz  20179  srglz  20180  srgisid  20181  rrgeq0i  20667  isdomn4  20684  islmodd  20852  rmodislmod  20916  islmhm2  21025  rnglidlmcl  21206  ip2eq  21643  mvrf1  21974  psdmul  22142  cply1mul  22271  isclo2  23063  cnpnei  23239  cncls  23249  lmss  23273  cnt0  23321  isnrm2  23333  isreg2  23352  tgcmp  23376  uncmp  23378  dfconn2  23394  1stcclb  23419  2ndcctbss  23430  comppfsc  23507  kgencn2  23532  ptpjpre1  23546  txlm  23623  kqfvima  23705  kqt0lem  23711  isr0  23712  nrmr0reg  23724  fgss2  23849  isufil2  23883  cfinufil  23903  flimopn  23950  fbflim2  23952  flfneii  23967  cnpflf  23976  fclssscls  23993  fclsnei  23994  fclsrest  23999  flimfnfcls  24003  fclscmp  24005  isfcf  24009  fcfnei  24010  alexsubALTlem3  24024  alexsubALTlem4  24025  alexsubALT  24026  tsmsgsum  24114  tsmsres  24119  tsmsxplem1  24128  ustincl  24183  ustdiag  24184  ustinvel  24185  ustexhalf  24186  cfiluexsm  24264  psmet0  24283  prdsbl  24466  metss  24483  metcnp3  24515  isngp4  24587  nmoi  24703  mulc1cncf  24882  cncfco  24884  lebnumii  24943  iscfil3  25250  iscau2  25254  iscau4  25256  equivcfil  25276  equivcau  25277  lmcau  25290  ismbf  25605  ellimc3  25856  lhop1  25991  dvfsumlem4  26006  dvfsum2  26011  dgrco  26250  fta1  26285  aalioulem2  26310  aalioulem4  26312  ulmclm  26365  ulmshftlem  26367  ulmcaulem  26372  ulmcau  26373  ulmcn  26377  cxploglim  26955  ftalem3  27052  chtub  27189  dchrelbasd  27216  2sqlem6  27400  2sqlem10  27405  dchrisumlema  27465  dchrisumlem2  27467  dchrisumlem3  27468  dchrvmasumlem2  27475  pntpbnd1  27563  pntibnd  27570  pntleml  27588  nolt02o  27673  noresle  27675  nosupbnd1lem1  27686  nosupbnd1lem4  27689  nosupbnd2lem1  27693  nosupbnd2  27694  nocvxminlem  27760  madebdaylemold  27904  n0subs  28369  z12zsodd  28488  brbtwn2  28988  colinearalg  28993  axcontlem4  29050  usgruspgrb  29266  cusgredg  29507  cusgrres  29532  usgredgsscusgredg  29543  fusgrn0degnn0  29583  wlk1walk  29722  wlkres  29752  wlkp1lem6  29760  wlkdlem2  29765  upgrwlkdvdelem  29819  pthdlem2lem  29850  lfgrn1cycl  29888  wwlksnredwwlkn  29978  wwlksnextproplem2  29993  clwwlkccatlem  30074  clwlkclwwlkf1lem3  30091  clwwisshclwwslemlem  30098  clwwlkf1  30134  clwwlkext2edg  30141  3cyclfrgrrn1  30370  n4cyclfrgr  30376  frgrwopregasn  30401  frgrwopregbsn  30402  isgrpo  30583  blocnilem  30890  ip2eqi  30942  htthlem  31003  hial0  31188  hial02  31189  hial2eq  31192  ocorth  31377  h1de2i  31639  pjjsi  31786  lnopunilem1  32096  lnophmlem1  32102  nmcexi  32112  riesz4i  32149  mdi  32381  mdbr3  32383  mdbr4  32384  dmdi  32388  dmdbr3  32391  dmdbr4  32392  dmdi4  32393  mdslmd1i  32415  atss  32432  atom1d  32439  atmd  32485  sumdmdlem2  32505  cdj1i  32519  cdj3i  32527  fnpreimac  32758  nn0min  32909  archiabllem1a  33267  archiabllem2a  33270  archiabl  33274  isarchiofld  33275  trisecnconstr  33952  crefi  34007  pcmplfin  34020  fmcncfil  34091  sigaclcu  34277  unelsiga  34294  sigapildsys  34322  ldgenpisys  34326  measvun  34369  carsgclctunlem2  34479  sibfima  34498  fnrelpredd  35250  fineqvnttrclse  35284  fineqvinfep  35285  pfxwlk  35322  derangenlem  35369  subfacp1lem6  35383  resconn  35444  cvmcov  35461  cvmliftlem3  35485  cvmliftphtlem  35515  satfdmfmla  35598  mclsax  35767  dfon2lem6  35984  fwddifnp1  36363  opnrebl2  36519  nn0prpwlem  36520  nn0prpw  36521  neibastop2lem  36558  neibastop2  36559  filnetlem4  36579  dfttc4  36728  bj-mooreset  37430  bj-ismoored0  37434  dfgcd3  37654  fin2so  37942  poimirlem25  37980  poimirlem29  37984  poimir  37988  mbfresfi  38001  ftc1cnnclem  38026  seqpo  38082  incsequz  38083  mettrifi  38092  geomcau  38094  caushft  38096  sstotbnd2  38109  equivtotbnd  38113  totbndbnd  38124  ismtybndlem  38141  heibor1lem  38144  bfplem2  38158  opidonOLD  38187  exidu1  38191  rngoideu  38238  isdrngo2  38293  unichnidl  38366  lsat0cv  39493  lcvexchlem4  39497  lcvexchlem5  39498  eqlkr3  39561  lub0N  39649  glb0N  39653  cvrnbtwn  39731  ltrneq2  40608  trlval2  40623  lpolsatN  41948  lpolpolsatN  41949  hdmap14lem12  42339  fsuppind  43037  nna4b4nsq  43107  incssnn0  43157  lnmlssfg  43526  unxpwdom3  43541  neik0pk1imk0  44492  ismnushort  44746  fnchoice  45478  monoordxrv  45927  monoord2xrv  45929  limcrecl  46077  fourierdlem54  46606  fourierdlem103  46655  fourierdlem104  46656  euoreqb  47569  smonoord  47837  iccpartlt  47896  iccpartgt  47899  iccpartdisj  47909  paireqne  47983  fmtnodvds  48019  perfectALTVlem2  48210  sbgoldbwt  48265  sbgoldbst  48266  sgoldbeven3prm  48271  mogoldbb  48273  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  bgoldbnnsum3prm  48292  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbndlem4  48296  bgoldbtbnd  48297  tgblthelfgott  48303  tgoldbach  48305  grimuhgr  48375  grimcnv  48376  grimco  48377  uhgrimedgi  48378  isuspgrim0  48382  upgrimwlklem5  48389  uhgrimisgrgriclem  48418  clnbgrgrimlem  48421  clnbgrgrim  48422  grimedg  48423  uspgrlimlem3  48478  uspgrlimlem4  48479  grlimedgclnbgr  48483  grlimgrtrilem2  48490  grlimgrtri  48491  grilcbri2  48499  grlicsym  48501  grlictr  48503  clnbgr3stgrgrlim  48507  clnbgr3stgrgrlic  48508  lcosslsp  48926  linindslinci  48936  lindslinindsimp1  48945  ldepsnlinclem1  48993  ldepsnlinclem2  48994  iscnrm3r  49435  initc  49578  termc2  50005