Theorem rspcv 3522

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2112  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056

This theorem is referenced by:  rspccv  3524  rspcva  3525  rspccva  3526  rspcdva  3529  rspc2v  3537  rspc3v  3540  rr19.3v  3566  rr19.28v  3567  rspsbc  3778  rspc2vd  3849  intmin  4865  ralxfrALT  5293  somo  5490  fr2nr  5514  weniso  7141  fr3nr  7535  limuni3  7609  tfinds  7616  funcnvuni  7687  suppfnss  7909  onnseq  8059  smo11  8079  tfrlem9  8099  tz7.49  8159  omeulem1  8288  oeordi  8293  nneneq  8807  frfi  8894  unblem2  8902  unbnn2  8906  xpfi  8920  ordiso2  9109  cantnflem1  9282  rankunb  9431  tcrank  9465  carduni  9562  dfac8alem  9608  alephinit  9674  aceq3lem  9699  dfac5  9707  dfac12r  9725  dfac12k  9726  pwsdompw  9783  cflm  9829  isf32lem1  9932  isf32lem2  9933  isf34lem4  9956  hsmexlem4  10008  axcc3  10017  domtriomlem  10021  axdc3lem2  10030  axdc4lem  10034  axcclem  10036  axdclem  10098  alephval2  10151  winainflem  10272  eltskm  10422  squeeze0  11700  lbreu  11747  nnsub  11839  ublbneg  12494  zmax  12506  zbtwnre  12507  xrub  12867  infmremnf  12898  infmrp1  12899  fzrevral  13162  axdc4uzlem  13521  faclbnd4lem4  13827  ccatalpha  14115  wrdind  14252  wrd2ind  14253  reuccatpfxs1lem  14276  recan  14865  cau3lem  14883  caubnd2  14886  climrlim2  15073  climshftlem  15100  rlimcld2  15104  subcn2  15121  isercoll  15196  climcau  15199  serf0  15209  iseralt  15213  isumrpcl  15370  clim2prod  15415  ntrivcvgfvn0  15426  sqrt2irr  15773  ndvdssub  15933  dfgcd2  16069  lcmf  16153  lcmfunsnlem1  16157  lcmfunsnlem2lem1  16158  lcmfunsnlem2lem2  16159  lcmfdvdsb  16163  coprmgcdb  16169  coprmdvds1  16172  coprmprod  16181  coprmproddvdslem  16182  nprm  16208  dvdsprm  16223  coprm  16231  pcmpt  16408  pcmptdvds  16410  pcfac  16415  prmpwdvds  16420  unbenlem  16424  vdwlem10  16506  vdwlem13  16509  vdwnnlem1  16511  prmdvdsprmop  16559  prmgaplem7  16573  catideu  17132  initoid  17461  termoid  17462  initoeu1  17471  termoeu1  17478  isdrs2  17767  lublecllem  17820  lubun  17975  lidrididd  18096  sgrp2rid2ex  18308  dfgrp2  18346  grpidinv2  18376  dfgrp3lem  18415  issubg4  18516  efgi  19063  efgi2  19069  dprdss  19370  srgrz  19495  srglz  19496  srgisid  19497  f1rhm0to0ALT  19715  islmodd  19859  rmodislmod  19921  islmhm2  20029  rrgeq0i  20281  ip2eq  20569  mvrf1  20904  cply1mul  21169  isclo2  21939  cnpnei  22115  cncls  22125  lmss  22149  cnt0  22197  isnrm2  22209  isreg2  22228  tgcmp  22252  uncmp  22254  dfconn2  22270  1stcclb  22295  2ndcctbss  22306  comppfsc  22383  kgencn2  22408  ptpjpre1  22422  txlm  22499  kqfvima  22581  kqt0lem  22587  isr0  22588  nrmr0reg  22600  fgss2  22725  isufil2  22759  cfinufil  22779  flimopn  22826  fbflim2  22828  flfneii  22843  cnpflf  22852  fclssscls  22869  fclsnei  22870  fclsrest  22875  flimfnfcls  22879  fclscmp  22881  isfcf  22885  fcfnei  22886  alexsubALTlem3  22900  alexsubALTlem4  22901  alexsubALT  22902  tsmsgsum  22990  tsmsres  22995  tsmsxplem1  23004  ustincl  23059  ustdiag  23060  ustinvel  23061  ustexhalf  23062  cfiluexsm  23141  psmet0  23160  prdsbl  23343  metss  23360  metcnp3  23392  isngp4  23464  nmoi  23580  mulc1cncf  23756  cncfco  23758  lebnumii  23817  iscfil3  24124  iscau2  24128  iscau4  24130  equivcfil  24150  equivcau  24151  lmcau  24164  ismbf  24479  ellimc3  24730  lhop1  24865  dvfsumlem4  24880  dvfsum2  24885  dgrco  25123  fta1  25155  aalioulem2  25180  aalioulem4  25182  ulmclm  25233  ulmshftlem  25235  ulmcaulem  25240  ulmcau  25241  ulmcn  25245  cxploglim  25814  ftalem3  25911  chtub  26047  dchrelbasd  26074  2sqlem6  26258  2sqlem10  26263  dchrisumlema  26323  dchrisumlem2  26325  dchrisumlem3  26326  dchrvmasumlem2  26333  pntpbnd1  26421  pntibnd  26428  pntleml  26446  brbtwn2  26950  colinearalg  26955  axcontlem4  27012  usgruspgrb  27226  cusgredg  27466  cusgrres  27490  usgredgsscusgredg  27501  fusgrn0degnn0  27541  wlk1walk  27680  wlkres  27712  wlkp1lem6  27720  wlkdlem2  27725  upgrwlkdvdelem  27777  pthdlem2lem  27808  lfgrn1cycl  27843  wwlksnredwwlkn  27933  wwlksnextproplem2  27948  clwwlkccatlem  28026  clwlkclwwlkf1lem3  28043  clwwisshclwwslemlem  28050  clwwlkf1  28086  clwwlkext2edg  28093  3cyclfrgrrn1  28322  n4cyclfrgr  28328  frgrwopregasn  28353  frgrwopregbsn  28354  isgrpo  28532  blocnilem  28839  ip2eqi  28891  htthlem  28952  hial0  29137  hial02  29138  hial2eq  29141  ocorth  29326  h1de2i  29588  pjjsi  29735  lnopunilem1  30045  lnophmlem1  30051  nmcexi  30061  riesz4i  30098  mdi  30330  mdbr3  30332  mdbr4  30333  dmdi  30337  dmdbr3  30340  dmdbr4  30341  dmdi4  30342  mdslmd1i  30364  atss  30381  atom1d  30388  atmd  30434  sumdmdlem2  30454  cdj1i  30468  cdj3i  30476  fnpreimac  30682  nn0min  30808  archiabllem1a  31118  archiabllem2a  31121  archiabl  31125  isarchiofld  31189  crefi  31465  pcmplfin  31478  fmcncfil  31549  sigaclcu  31751  unelsiga  31768  sigapildsys  31796  ldgenpisys  31800  measvun  31843  carsgclctunlem2  31952  sibfima  31971  fnrelpredd  32728  pfxwlk  32752  derangenlem  32800  subfacp1lem6  32814  resconn  32875  cvmcov  32892  cvmliftlem3  32916  cvmliftphtlem  32946  satfdmfmla  33029  mclsax  33198  dfon2lem6  33434  poseq  33482  soseq  33483  naddelim  33524  nolt02o  33584  noresle  33586  nosupbnd1lem1  33597  nosupbnd1lem4  33600  nosupbnd2lem1  33604  nosupbnd2  33605  nocvxminlem  33658  madebdaylemold  33764  fwddifnp1  34153  opnrebl2  34196  nn0prpwlem  34197  nn0prpw  34198  neibastop2lem  34235  neibastop2  34236  filnetlem4  34256  bj-mooreset  34957  bj-ismoored0  34961  dfgcd3  35178  fin2so  35450  poimirlem25  35488  poimirlem29  35492  poimir  35496  mbfresfi  35509  ftc1cnnclem  35534  seqpo  35591  incsequz  35592  mettrifi  35601  geomcau  35603  caushft  35605  sstotbnd2  35618  equivtotbnd  35622  totbndbnd  35633  ismtybndlem  35650  heibor1lem  35653  bfplem2  35667  opidonOLD  35696  exidu1  35700  rngoideu  35747  isdrngo2  35802  unichnidl  35875  lsat0cv  36733  lcvexchlem4  36737  lcvexchlem5  36738  eqlkr3  36801  lub0N  36889  glb0N  36893  cvrnbtwn  36971  ltrneq2  37848  trlval2  37863  lpolsatN  39188  lpolpolsatN  39189  hdmap14lem12  39579  isdomn4  39835  fsuppind  39930  nna4b4nsq  40141  incssnn0  40177  lnmlssfg  40549  unxpwdom3  40564  neik0pk1imk0  41275  ismnushort  41533  fnchoice  42186  monoordxrv  42638  monoord2xrv  42640  limcrecl  42788  fourierdlem54  43319  fourierdlem103  43368  fourierdlem104  43369  euoreqb  44216  smonoord  44439  iccpartlt  44492  iccpartgt  44495  iccpartdisj  44505  paireqne  44579  fmtnodvds  44612  perfectALTVlem2  44790  sbgoldbwt  44845  sbgoldbst  44846  sgoldbeven3prm  44851  mogoldbb  44853  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  bgoldbnnsum3prm  44872  bgoldbtbndlem2  44874  bgoldbtbndlem3  44875  bgoldbtbndlem4  44876  bgoldbtbnd  44877  tgblthelfgott  44883  tgoldbach  44885  isomuspgrlem2c  44898  isomuspgrlem2d  44899  lcosslsp  45395  linindslinci  45405  lindslinindsimp1  45414  ldepsnlinclem1  45462  ldepsnlinclem2  45463  iscnrm3r  45858