Theorem rspcv 3574

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 3570	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  3575  rspcva  3576  rspccva  3577  rspcdva  3579  rspc2v  3589  rspc3v  3594  rspc4v  3598  rr19.3v  3623  rr19.28v  3624  rspsbc  3831  rspc2vd  3899  intmin  4925  ralxfrALT  5362  somo  5579  fr2nr  5609  weniso  7310  fr3nr  7727  limuni3  7804  tfinds  7812  funcnvuni  7884  resf1extb  7886  poseq  8110  soseq  8111  suppfnss  8141  onnseq  8286  smo11  8306  tfrlem9  8326  tz7.49  8386  omeulem1  8519  oeordi  8525  naddelim  8624  nneneq  9142  frfi  9197  unblem2  9205  unbnn2  9209  ordiso2  9432  cantnflem1  9610  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  frins3  9679  rankunb  9774  tcrank  9808  carduni  9905  dfac8alem  9951  alephinit  10017  aceq3lem  10042  dfac5  10051  dfac12r  10069  dfac12k  10070  pwsdompw  10125  cflm  10172  isf32lem1  10275  isf32lem2  10276  isf34lem4  10299  hsmexlem4  10351  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc4lem  10377  axcclem  10379  axdclem  10441  alephval2  10495  winainflem  10616  eltskm  10766  squeeze0  12057  lbreu  12104  nnsub  12201  ublbneg  12858  zmax  12870  zbtwnre  12871  xrub  13239  infmremnf  13271  infmrp1  13272  fzrevral  13540  axdc4uzlem  13918  faclbnd4lem4  14231  ccatalpha  14529  wrdind  14657  wrd2ind  14658  reuccatpfxs1lem  14681  recan  15272  cau3lem  15290  caubnd2  15293  climrlim2  15482  climshftlem  15509  rlimcld2  15513  subcn2  15530  isercoll  15603  climcau  15606  serf0  15616  iseralt  15620  isumrpcl  15778  clim2prod  15823  ntrivcvgfvn0  15834  sqrt2irr  16186  ndvdssub  16348  dfgcd2  16485  lcmf  16572  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfdvdsb  16582  coprmgcdb  16588  coprmdvds1  16591  coprmprod  16600  coprmproddvdslem  16601  nprm  16627  dvdsprm  16642  coprm  16650  pcmpt  16832  pcmptdvds  16834  pcfac  16839  prmpwdvds  16844  unbenlem  16848  vdwlem10  16930  vdwlem13  16933  vdwnnlem1  16935  prmdvdsprmop  16983  prmgaplem7  16997  catideu  17610  initoid  17937  termoid  17938  initoeu1  17947  termoeu1  17954  isdrs2  18241  lublecllem  18293  lubun  18450  lidrididd  18607  sgrp2rid2ex  18864  dfgrp2  18904  grpidinv2  18939  dfgrp3lem  18980  issubg4  19087  efgi  19660  efgi2  19666  dprdss  19972  srgrz  20154  srglz  20155  srgisid  20156  rrgeq0i  20644  isdomn4  20661  islmodd  20829  rmodislmod  20893  islmhm2  21002  rnglidlmcl  21183  ip2eq  21620  mvrf1  21953  psdmul  22121  cply1mul  22252  isclo2  23044  cnpnei  23220  cncls  23230  lmss  23254  cnt0  23302  isnrm2  23314  isreg2  23333  tgcmp  23357  uncmp  23359  dfconn2  23375  1stcclb  23400  2ndcctbss  23411  comppfsc  23488  kgencn2  23513  ptpjpre1  23527  txlm  23604  kqfvima  23686  kqt0lem  23692  isr0  23693  nrmr0reg  23705  fgss2  23830  isufil2  23864  cfinufil  23884  flimopn  23931  fbflim2  23933  flfneii  23948  cnpflf  23957  fclssscls  23974  fclsnei  23975  fclsrest  23980  flimfnfcls  23984  fclscmp  23986  isfcf  23990  fcfnei  23991  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  tsmsgsum  24095  tsmsres  24100  tsmsxplem1  24109  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  cfiluexsm  24245  psmet0  24264  prdsbl  24447  metss  24464  metcnp3  24496  isngp4  24568  nmoi  24684  mulc1cncf  24866  cncfco  24868  lebnumii  24933  iscfil3  25241  iscau2  25245  iscau4  25247  equivcfil  25267  equivcau  25268  lmcau  25281  ismbf  25597  ellimc3  25848  lhop1  25987  dvfsumlem4  26004  dvfsum2  26009  dgrco  26249  fta1  26284  aalioulem2  26309  aalioulem4  26311  ulmclm  26364  ulmshftlem  26366  ulmcaulem  26371  ulmcau  26372  ulmcn  26376  cxploglim  26956  ftalem3  27053  chtub  27191  dchrelbasd  27218  2sqlem6  27402  2sqlem10  27407  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  dchrvmasumlem2  27477  pntpbnd1  27565  pntibnd  27572  pntleml  27590  nolt02o  27675  noresle  27677  nosupbnd1lem1  27688  nosupbnd1lem4  27691  nosupbnd2lem1  27695  nosupbnd2  27696  nocvxminlem  27762  madebdaylemold  27906  n0subs  28371  z12zsodd  28490  brbtwn2  28990  colinearalg  28995  axcontlem4  29052  usgruspgrb  29268  cusgredg  29509  cusgrres  29534  usgredgsscusgredg  29545  fusgrn0degnn0  29585  wlk1walk  29724  wlkres  29754  wlkp1lem6  29762  wlkdlem2  29767  upgrwlkdvdelem  29821  pthdlem2lem  29852  lfgrn1cycl  29890  wwlksnredwwlkn  29980  wwlksnextproplem2  29995  clwwlkccatlem  30076  clwlkclwwlkf1lem3  30093  clwwisshclwwslemlem  30100  clwwlkf1  30136  clwwlkext2edg  30143  3cyclfrgrrn1  30372  n4cyclfrgr  30378  frgrwopregasn  30403  frgrwopregbsn  30404  isgrpo  30585  blocnilem  30892  ip2eqi  30944  htthlem  31005  hial0  31190  hial02  31191  hial2eq  31194  ocorth  31379  h1de2i  31641  pjjsi  31788  lnopunilem1  32098  lnophmlem1  32104  nmcexi  32114  riesz4i  32151  mdi  32383  mdbr3  32385  mdbr4  32386  dmdi  32390  dmdbr3  32393  dmdbr4  32394  dmdi4  32395  mdslmd1i  32417  atss  32434  atom1d  32441  atmd  32487  sumdmdlem2  32507  cdj1i  32521  cdj3i  32529  fnpreimac  32760  nn0min  32912  archiabllem1a  33285  archiabllem2a  33288  archiabl  33292  isarchiofld  33293  trisecnconstr  33970  crefi  34025  pcmplfin  34038  fmcncfil  34109  sigaclcu  34295  unelsiga  34312  sigapildsys  34340  ldgenpisys  34344  measvun  34387  carsgclctunlem2  34497  sibfima  34516  fnrelpredd  35268  fineqvnttrclse  35302  fineqvinfep  35303  pfxwlk  35340  derangenlem  35387  subfacp1lem6  35401  resconn  35462  cvmcov  35479  cvmliftlem3  35503  cvmliftphtlem  35533  satfdmfmla  35616  mclsax  35785  dfon2lem6  36002  fwddifnp1  36381  opnrebl2  36537  nn0prpwlem  36538  nn0prpw  36539  neibastop2lem  36576  neibastop2  36577  filnetlem4  36597  bj-mooreset  37355  bj-ismoored0  37359  dfgcd3  37579  fin2so  37858  poimirlem25  37896  poimirlem29  37900  poimir  37904  mbfresfi  37917  ftc1cnnclem  37942  seqpo  37998  incsequz  37999  mettrifi  38008  geomcau  38010  caushft  38012  sstotbnd2  38025  equivtotbnd  38029  totbndbnd  38040  ismtybndlem  38057  heibor1lem  38060  bfplem2  38074  opidonOLD  38103  exidu1  38107  rngoideu  38154  isdrngo2  38209  unichnidl  38282  lsat0cv  39409  lcvexchlem4  39413  lcvexchlem5  39414  eqlkr3  39477  lub0N  39565  glb0N  39569  cvrnbtwn  39647  ltrneq2  40524  trlval2  40539  lpolsatN  41864  lpolpolsatN  41865  hdmap14lem12  42255  fsuppind  42948  nna4b4nsq  43018  incssnn0  43068  lnmlssfg  43437  unxpwdom3  43452  neik0pk1imk0  44403  ismnushort  44657  fnchoice  45389  monoordxrv  45839  monoord2xrv  45841  limcrecl  45989  fourierdlem54  46518  fourierdlem103  46567  fourierdlem104  46568  euoreqb  47469  smonoord  47731  iccpartlt  47784  iccpartgt  47787  iccpartdisj  47797  paireqne  47871  fmtnodvds  47904  perfectALTVlem2  48082  sbgoldbwt  48137  sbgoldbst  48138  sgoldbeven3prm  48143  mogoldbb  48145  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  bgoldbnnsum3prm  48164  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbndlem4  48168  bgoldbtbnd  48169  tgblthelfgott  48175  tgoldbach  48177  grimuhgr  48247  grimcnv  48248  grimco  48249  uhgrimedgi  48250  isuspgrim0  48254  upgrimwlklem5  48261  uhgrimisgrgriclem  48290  clnbgrgrimlem  48293  clnbgrgrim  48294  grimedg  48295  uspgrlimlem3  48350  uspgrlimlem4  48351  grlimedgclnbgr  48355  grlimgrtrilem2  48362  grlimgrtri  48363  grilcbri2  48371  grlicsym  48373  grlictr  48375  clnbgr3stgrgrlim  48379  clnbgr3stgrgrlic  48380  lcosslsp  48798  linindslinci  48808  lindslinindsimp1  48817  ldepsnlinclem1  48865  ldepsnlinclem2  48866  iscnrm3r  49307  initc  49450  termc2  49877