Theorem rspcv 3573

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is used by:  rspccv  3574  rspcva  3575  rspccva  3576  rspcdva  3578  rspc2v  3587  rspc3v  3592  rspc4v  3596  rr19.3v  3621  rr19.28v  3622  rspsbc  3826  rspc2vd  3895  intmin  4928  ralxfrALT  5377  somo  5598  fr2nr  5628  weniso  7362  fr3nr  7784  limuni3  7861  tfinds  7869  funcnvuni  7942  resf1extb  7944  poseq  8168  soseq  8169  suppfnss  8199  onnseq  8345  smo11  8365  tfrlem9  8386  tz7.49  8448  omeulem1  8583  oeordi  8589  naddelim  8689  nneneq  9214  frfi  9269  unblem2  9278  unbnn2  9282  ordiso2  9502  cantnflem1  9683  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  frins3  9752  rankunb  9857  tcrank  9894  scottex  9926  carduni  10055  dfac8alem  10101  alephinit  10167  aceq3lem  10192  dfac5  10200  dfac12r  10218  dfac12k  10219  pwsdompw  10274  cflm  10320  isf32lem1  10424  isf32lem2  10425  isf34lem4  10448  hsmexlem4  10500  axcc3  10509  domtriomlem  10513  axdc3lem2  10522  axdc4lem  10526  axcclem  10528  axdclem  10590  alephval2  10650  winainflem  10771  eltskm  10921  squeeze0  12213  lbreu  12260  nnsub  12375  ublbneg  13053  zmax  13065  zbtwnre  13066  xrub  13435  infmremnf  13467  infmrp1  13468  fzrevral  13739  axdc4uzlem  14119  faclbnd4lem4  14433  ccatalpha  14733  wrdind  14864  wrd2ind  14865  reuccatpfxs1lem  14888  recan  15497  cau3lem  15515  caubnd2  15518  climrlim2  15707  climshftlem  15734  rlimcld2  15738  subcn2  15755  isercoll  15828  climcau  15831  serf0  15841  iseralt  15845  isumrpcl  16005  clim2prod  16050  ntrivcvgfvn0  16061  sqrt2irr  16410  ndvdssub  16572  dfgcd2  16712  lcmf  16801  lcmfunsnlem1  16805  lcmfunsnlem2lem1  16806  lcmfunsnlem2lem2  16807  lcmfdvdsb  16811  coprmgcdb  16817  coprmdvds1  16820  coprmprod  16829  coprmproddvdslem  16830  nprm  16856  dvdsprm  16872  coprm  16880  pcmpt  17063  pcmptdvds  17065  pcfac  17070  prmpwdvds  17075  unbenlem  17079  vdwlem10  17161  vdwlem13  17164  vdwnnlem1  17166  prmdvdsprmop  17214  prmgaplem7  17228  catideu  17842  initoid  18169  termoid  18170  initoeu1  18179  termoeu1  18186  isdrs2  18473  lublecllem  18525  lubun  18682  lidrididd  18844  mgmidpfod  18850  sgrp2rid2ex  19119  dfgrp2  19166  grpidinv2  19201  dfgrp3lem  19241  issubg4  19349  efgi  19926  efgi2  19932  dprdss  20238  srgrz  20426  srglz  20427  srgisid  20428  rrgeq0i  20944  isdomn4  20960  isdrng3lem2  20999  islmodd  21134  rmodislmod  21198  islmhm2  21306  rnglidlmcl  21488  ip2eq  21952  mvrf1  22286  psdmul  22480  cply1mul  22607  isclo2  23399  cnpnei  23575  cncls  23585  lmss  23609  cnt0  23657  isnrm2  23669  isreg2  23688  tgcmp  23712  uncmp  23714  dfconn2  23730  1stcclb  23755  2ndcctbss  23767  comppfsc  23844  kgencn2  23869  ptpjpre1  23883  txlm  23960  kqfvima  24042  kqt0lem  24048  isr0  24049  nrmr0reg  24061  fgss2  24186  isufil2  24220  cfinufil  24240  flimopn  24287  fbflim2  24289  flfneii  24304  cnpflf  24313  fclssscls  24330  fclsnei  24331  fclsrest  24336  flimfnfcls  24340  fclscmp  24342  isfcf  24346  fcfnei  24347  alexsubALTlem3  24361  alexsubALTlem4  24362  alexsubALT  24363  tsmsgsum  24451  tsmsres  24456  tsmsxplem1  24465  ustincl  24520  ustdiag  24521  ustinvel  24522  ustexhalf  24523  cfiluexsm  24601  psmet0  24620  prdsbl  24803  metss  24820  metcnp3  24852  isngp4  24924  nmoi  25040  mulc1cncf  25219  cncfco  25221  lebnumii  25280  iscfil3  25587  iscau2  25591  iscau4  25593  equivcfil  25613  equivcau  25614  lmcau  25627  ismbf  25942  ellimc3  26192  lhop1  26327  dvfsumlem4  26342  dvfsum2  26347  dgrco  26587  fta1  26622  plyconz  26624  aalioulem2  26653  aalioulem4  26655  ulmclm  26707  ulmshftlem  26709  ulmcaulem  26714  ulmcau  26715  ulmcn  26719  cxploglim  27298  ftalem3  27395  chtub  27532  dchrelbasd  27559  2sqlem6  27743  2sqlem10  27748  dchrisumlema  27808  dchrisumlem2  27810  dchrisumlem3  27811  dchrvmasumlem2  27818  pntpbnd1  27906  pntibnd  27913  pntleml  27931  nna4b4nsq  27983  fltoprm  27988  nolt02o  28045  noresle  28047  nosupbnd1lem1  28058  nosupbnd1lem4  28061  nosupbnd2lem1  28065  nosupbnd2  28066  nocvxminlem  28133  madebdaylemold  28277  n0subs  28742  z12zsodd  28861  brbtwn2  29476  colinearalg  29481  axcontlem4  29538  usgruspgrb  29757  cusgredg  29998  cusgrres  30022  usgredgsscusgredg  30033  fusgrn0degnn0  30073  wlk1walk  30212  wlkres  30242  wlkp1lem6  30250  wlkdlem2  30255  pfxwlk  30259  upgrwlkdvdelem  30315  pthdlem2lem  30346  lfgrn1cycl  30387  wwlksnredwwlkn  30477  wwlksnextproplem2  30492  clwwlkccatlem  30573  clwlkclwwlkf1lem3  30590  clwwisshclwwslemlem  30597  clwwlkf1  30633  clwwlkext2edg  30640  3cyclfrgrrn1  30879  n4cyclfrgr  30885  frgrwopregasn  30910  frgrwopregbsn  30911  isgrpo  31092  blocnilem  31399  ip2eqi  31451  htthlem  31512  hial0  31697  hial02  31698  hial2eq  31701  ocorth  31886  h1de2i  32148  pjjsi  32295  lnopunilem1  32605  lnophmlem1  32611  nmcexi  32621  riesz4i  32658  mdi  32890  mdbr3  32892  mdbr4  32893  dmdi  32897  dmdbr3  32900  dmdbr4  32901  dmdi4  32902  mdslmd1i  32924  atss  32941  atom1d  32948  atmd  32994  sumdmdlem2  33014  cdj1i  33028  cdj3i  33036  fnpreimac  33257  nn0min  33405  archiabllem1a  33745  archiabllem2a  33748  archiabl  33752  isarchiofld  33753  trisecnconstr  34417  crefi  34472  pcmplfin  34485  fmcncfil  34556  sigaclcu  34742  unelsiga  34759  sigapildsys  34788  ldgenpisys  34792  measvun  34835  carsgclctunlem2  34944  sibfima  34963  fnrelpredd  35709  fineqvnttrclse  35775  fineqvinfep  35776  derangenlem  35915  subfacp1lem6  35929  resconn  35990  cvmcov  36007  cvmliftlem3  36031  cvmliftphtlem  36061  satfdmfmla  36144  mclsax  36313  dfon2lem6  36530  fwddifnp1  36910  opnrebl2  37089  nn0prpwlem  37090  nn0prpw  37091  neibastop2lem  37128  neibastop2  37129  filnetlem4  37149  dfttc4  37298  bj-mooreset  38003  bj-ismoored0  38007  dfgcd3  38225  fin2so  38510  poimirlem25  38543  poimirlem29  38547  poimir  38551  mbfresfi  38564  ftc1cnnclem  38589  seqpo  38661  incsequz  38662  mettrifi  38671  geomcau  38673  caushft  38675  sstotbnd2  38688  equivtotbnd  38692  totbndbnd  38703  ismtybndlem  38720  heibor1lem  38723  bfplem2  38737  opidonOLD  38766  exidu1  38770  rngoideu  38817  isdrngo2  38872  unichnidl  38945  lsat0cv  40070  lcvexchlem4  40074  lcvexchlem5  40075  eqlkr3  40138  lub0N  40226  glb0N  40230  cvrnbtwn  40308  ltrneq2  41185  trlval2  41200  lpolsatN  42525  lpolpolsatN  42526  hdmap14lem12  42916  fsuppind  43598  incssnn0  43701  lnmlssfg  44066  unxpwdom3  44081  neik0pk1imk0  45032  ismnushort  45270  fnchoice  46015  monoordxrv  46460  monoord2xrv  46462  limcrecl  46610  fourierdlem54  47139  fourierdlem103  47188  fourierdlem104  47189  euoreqb  48148  smonoord  48416  iccpartlt  48475  iccpartgt  48478  iccpartdisj  48488  paireqne  48562  fmtnodvds  48598  perfectALTVlem2  48789  sbgoldbwt  48844  sbgoldbst  48845  sgoldbeven3prm  48850  mogoldbb  48852  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  bgoldbnnsum3prm  48871  bgoldbtbndlem2  48873  bgoldbtbndlem3  48874  bgoldbtbndlem4  48875  bgoldbtbnd  48876  tgblthelfgott  48882  tgoldbach  48884  grimuhgr  48954  grimcnv  48955  grimco  48956  uhgrimedgi  48957  isuspgrim0  48961  upgrimwlklem5  48968  uhgrimisgrgriclem  48997  clnbgrgrimlem  49000  clnbgrgrim  49001  grimedg  49002  uspgrlimlem3  49057  uspgrlimlem4  49058  grlimedgclnbgr  49062  grlimgrtrilem2  49069  grlimgrtri  49070  grilcbri2  49078  grlicsym  49080  grlictr  49082  clnbgr3stgrgrlim  49086  clnbgr3stgrgrlic  49087  lcosslsp  49519  linindslinci  49529  lindslinindsimp1  49538  ldepsnlinclem1  49586  ldepsnlinclem2  49587  iscnrm3r  50025  initc  50168  termc2  50595  nellindf  50939