Theorem rspcv 3584

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 3580	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  3585  rspcva  3586  rspccva  3587  rspcdva  3589  rspc2v  3599  rspc3v  3604  rspc4v  3608  rr19.3v  3633  rr19.28v  3634  rspsbc  3842  rspc2vd  3910  intmin  4932  ralxfrALT  5370  somo  5585  fr2nr  5615  weniso  7329  fr3nr  7748  limuni3  7828  tfinds  7836  funcnvuni  7908  resf1extb  7910  poseq  8137  soseq  8138  suppfnss  8168  onnseq  8313  smo11  8333  tfrlem9  8353  tz7.49  8413  omeulem1  8546  oeordi  8551  naddelim  8650  nneneq  9170  frfi  9232  unblem2  9240  unbnn2  9244  xpfiOLD  9270  ordiso2  9468  cantnflem1  9642  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  frins3  9708  rankunb  9803  tcrank  9837  carduni  9934  dfac8alem  9982  alephinit  10048  aceq3lem  10073  dfac5  10082  dfac12r  10100  dfac12k  10101  pwsdompw  10156  cflm  10203  isf32lem1  10306  isf32lem2  10307  isf34lem4  10330  hsmexlem4  10382  axcc3  10391  domtriomlem  10395  axdc3lem2  10404  axdc4lem  10408  axcclem  10410  axdclem  10472  alephval2  10525  winainflem  10646  eltskm  10796  squeeze0  12086  lbreu  12133  nnsub  12230  ublbneg  12892  zmax  12904  zbtwnre  12905  xrub  13272  infmremnf  13304  infmrp1  13305  fzrevral  13573  axdc4uzlem  13948  faclbnd4lem4  14261  ccatalpha  14558  wrdind  14687  wrd2ind  14688  reuccatpfxs1lem  14711  recan  15303  cau3lem  15321  caubnd2  15324  climrlim2  15513  climshftlem  15540  rlimcld2  15544  subcn2  15561  isercoll  15634  climcau  15637  serf0  15647  iseralt  15651  isumrpcl  15809  clim2prod  15854  ntrivcvgfvn0  15865  sqrt2irr  16217  ndvdssub  16379  dfgcd2  16516  lcmf  16603  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfdvdsb  16613  coprmgcdb  16619  coprmdvds1  16622  coprmprod  16631  coprmproddvdslem  16632  nprm  16658  dvdsprm  16673  coprm  16681  pcmpt  16863  pcmptdvds  16865  pcfac  16870  prmpwdvds  16875  unbenlem  16879  vdwlem10  16961  vdwlem13  16964  vdwnnlem1  16966  prmdvdsprmop  17014  prmgaplem7  17028  catideu  17636  initoid  17963  termoid  17964  initoeu1  17973  termoeu1  17980  isdrs2  18267  lublecllem  18319  lubun  18474  lidrididd  18597  sgrp2rid2ex  18854  dfgrp2  18894  grpidinv2  18929  dfgrp3lem  18970  issubg4  19077  efgi  19649  efgi2  19655  dprdss  19961  srgrz  20116  srglz  20117  srgisid  20118  rrgeq0i  20608  isdomn4  20625  islmodd  20772  rmodislmod  20836  islmhm2  20945  rnglidlmcl  21126  ip2eq  21562  mvrf1  21895  psdmul  22053  cply1mul  22183  isclo2  22975  cnpnei  23151  cncls  23161  lmss  23185  cnt0  23233  isnrm2  23245  isreg2  23264  tgcmp  23288  uncmp  23290  dfconn2  23306  1stcclb  23331  2ndcctbss  23342  comppfsc  23419  kgencn2  23444  ptpjpre1  23458  txlm  23535  kqfvima  23617  kqt0lem  23623  isr0  23624  nrmr0reg  23636  fgss2  23761  isufil2  23795  cfinufil  23815  flimopn  23862  fbflim2  23864  flfneii  23879  cnpflf  23888  fclssscls  23905  fclsnei  23906  fclsrest  23911  flimfnfcls  23915  fclscmp  23917  isfcf  23921  fcfnei  23922  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  tsmsgsum  24026  tsmsres  24031  tsmsxplem1  24040  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  cfiluexsm  24177  psmet0  24196  prdsbl  24379  metss  24396  metcnp3  24428  isngp4  24500  nmoi  24616  mulc1cncf  24798  cncfco  24800  lebnumii  24865  iscfil3  25173  iscau2  25177  iscau4  25179  equivcfil  25199  equivcau  25200  lmcau  25213  ismbf  25529  ellimc3  25780  lhop1  25919  dvfsumlem4  25936  dvfsum2  25941  dgrco  26181  fta1  26216  aalioulem2  26241  aalioulem4  26243  ulmclm  26296  ulmshftlem  26298  ulmcaulem  26303  ulmcau  26304  ulmcn  26308  cxploglim  26888  ftalem3  26985  chtub  27123  dchrelbasd  27150  2sqlem6  27334  2sqlem10  27339  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  dchrvmasumlem2  27409  pntpbnd1  27497  pntibnd  27504  pntleml  27522  nolt02o  27607  noresle  27609  nosupbnd1lem1  27620  nosupbnd1lem4  27623  nosupbnd2lem1  27627  nosupbnd2  27628  nocvxminlem  27689  madebdaylemold  27809  n0subs  28253  brbtwn2  28832  colinearalg  28837  axcontlem4  28894  usgruspgrb  29110  cusgredg  29351  cusgrres  29376  usgredgsscusgredg  29387  fusgrn0degnn0  29427  wlk1walk  29567  wlkres  29598  wlkp1lem6  29606  wlkdlem2  29611  upgrwlkdvdelem  29666  pthdlem2lem  29697  lfgrn1cycl  29735  wwlksnredwwlkn  29825  wwlksnextproplem2  29840  clwwlkccatlem  29918  clwlkclwwlkf1lem3  29935  clwwisshclwwslemlem  29942  clwwlkf1  29978  clwwlkext2edg  29985  3cyclfrgrrn1  30214  n4cyclfrgr  30220  frgrwopregasn  30245  frgrwopregbsn  30246  isgrpo  30426  blocnilem  30733  ip2eqi  30785  htthlem  30846  hial0  31031  hial02  31032  hial2eq  31035  ocorth  31220  h1de2i  31482  pjjsi  31629  lnopunilem1  31939  lnophmlem1  31945  nmcexi  31955  riesz4i  31992  mdi  32224  mdbr3  32226  mdbr4  32227  dmdi  32231  dmdbr3  32234  dmdbr4  32235  dmdi4  32236  mdslmd1i  32258  atss  32275  atom1d  32282  atmd  32328  sumdmdlem2  32348  cdj1i  32362  cdj3i  32370  fnpreimac  32595  nn0min  32745  archiabllem1a  33145  archiabllem2a  33148  archiabl  33152  isarchiofld  33295  trisecnconstr  33782  crefi  33837  pcmplfin  33850  fmcncfil  33921  sigaclcu  34107  unelsiga  34124  sigapildsys  34152  ldgenpisys  34156  measvun  34199  carsgclctunlem2  34310  sibfima  34329  fnrelpredd  35079  pfxwlk  35111  derangenlem  35158  subfacp1lem6  35172  resconn  35233  cvmcov  35250  cvmliftlem3  35274  cvmliftphtlem  35304  satfdmfmla  35387  mclsax  35556  dfon2lem6  35776  fwddifnp1  36153  opnrebl2  36309  nn0prpwlem  36310  nn0prpw  36311  neibastop2lem  36348  neibastop2  36349  filnetlem4  36369  bj-mooreset  37090  bj-ismoored0  37094  dfgcd3  37312  fin2so  37601  poimirlem25  37639  poimirlem29  37643  poimir  37647  mbfresfi  37660  ftc1cnnclem  37685  seqpo  37741  incsequz  37742  mettrifi  37751  geomcau  37753  caushft  37755  sstotbnd2  37768  equivtotbnd  37772  totbndbnd  37783  ismtybndlem  37800  heibor1lem  37803  bfplem2  37817  opidonOLD  37846  exidu1  37850  rngoideu  37897  isdrngo2  37952  unichnidl  38025  lsat0cv  39026  lcvexchlem4  39030  lcvexchlem5  39031  eqlkr3  39094  lub0N  39182  glb0N  39186  cvrnbtwn  39264  ltrneq2  40142  trlval2  40157  lpolsatN  41482  lpolpolsatN  41483  hdmap14lem12  41873  fsuppind  42578  nna4b4nsq  42648  incssnn0  42699  lnmlssfg  43069  unxpwdom3  43084  neik0pk1imk0  44036  ismnushort  44290  fnchoice  45023  monoordxrv  45477  monoord2xrv  45479  limcrecl  45627  fourierdlem54  46158  fourierdlem103  46207  fourierdlem104  46208  euoreqb  47110  smonoord  47372  iccpartlt  47425  iccpartgt  47428  iccpartdisj  47438  paireqne  47512  fmtnodvds  47545  perfectALTVlem2  47723  sbgoldbwt  47778  sbgoldbst  47779  sgoldbeven3prm  47784  mogoldbb  47786  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  bgoldbnnsum3prm  47805  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgblthelfgott  47816  tgoldbach  47818  grimuhgr  47887  grimcnv  47888  grimco  47889  uhgrimedgi  47890  isuspgrim0  47894  upgrimwlklem5  47901  uhgrimisgrgriclem  47930  clnbgrgrimlem  47933  clnbgrgrim  47934  grimedg  47935  uspgrlimlem3  47989  uspgrlimlem4  47990  grlimgrtrilem2  47994  grlimgrtri  47995  grilcbri2  48003  grlicsym  48005  grlictr  48007  clnbgr3stgrgrlic  48011  lcosslsp  48427  linindslinci  48437  lindslinindsimp1  48446  ldepsnlinclem1  48494  ldepsnlinclem2  48495  iscnrm3r  48936  initc  49080  termc2  49507