Theorem rspcva 3568

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcva	⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3566	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	imp 407	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063

This theorem is referenced by:  rexraleqim  3586  fvn0ssdmfun  6992  fveqdmss  6996  fvcofneq  7009  wfr3g  8187  boxriin  8778  boxcutc  8779  marypha1lem  9269  supmo  9288  infmo  9331  unwdomg  9420  frr3g  9592  isinffi  9828  axdc3lem2  10287  grothac  10666  nqereu  10765  nnsub  12097  zextle  12473  xrsupsslem  13121  xrinfmsslem  13122  supxrunb1  13133  supxrunb2  13134  injresinjlem  13587  ssnn0fi  13785  suppssfz  13794  faclbnd4lem4  14090  ishashinf  14256  rexuz3  15139  cau3lem  15145  caubnd2  15148  o1co  15374  climcn1  15380  incexclem  15627  dvdsext  16109  mreintcl  17381  initoeu1  17803  initoeu2  17808  termoeu1  17810  lublecllem  18155  mgmidmo  18421  gsumval2  18447  dfgrp3lem  18749  symgfix2  19100  odeq  19234  gexid  19262  gsummoncoe1  21558  m2detleiblem3  21861  m2detleiblem4  21862  cpmatmcllem  21950  mp2pm2mplem4  22041  cayleyhamilton1  22124  cmpsublem  22633  cmpsub  22634  cmpfii  22643  ptpjcn  22845  isufil2  23142  ufileu  23153  lmmbr  24505  caussi  24544  plyco0  25436  dgrco  25519  emcllem7  26234  isppw2  26347  uvtxnbgrvtx  27896  rusgrnumwwlks  28475  clwwlkf  28547  vdgn1frgrv2  28796  frgrregorufr  28825  grpoidinvlem3  29004  grpoideu  29007  lnconi  30531  fsumiunle  31278  rngurd  31617  tpr2rico  32002  esumiun  32202  0elsiga  32222  sigaclci  32240  dya2icoseg2  32385  derangsn  33271  sat1el2xp  33480  addsid1  34201  fwddifnp1  34541  poimirlem25  35874  poimirlem26  35875  poimirlem30  35879  poimirlem31  35880  poimirlem32  35881  heicant  35884  mblfinlem2  35887  ftc1anc  35930  fdc  35975  bndss  36016  isdrngo2  36188  divrngidl  36258  maxidlmax  36273  cdleme0nex  38525  dihglblem2N  39529  hgmapvs  40126  ismrcd1  40736  nacsfg  40743  isnacs3  40748  nacsfix  40750  mzpcl1  40767  mzpcl2  40768  mzpcong  41011  dnnumch1  41086  aomclem1  41096  aomclem6  41101  lnr2i  41158  hbtlem5  41170  hbt  41172  pwssfi  42827  rexanuz3  42880  choicefi  42981  fsneq  42987  suplesup  43127  xralrple2  43142  infxr  43155  infleinf  43160  xralrple4  43161  xralrple3  43162  xrralrecnnge  43179  supxrunb3  43188  supxrleubrnmpt  43195  unb2ltle  43204  suprleubrnmpt  43211  infxrgelbrnmpt  43243  supminfxr  43253  xrpnf  43275  islpcn  43430  limclner  43442  climd  43463  clim2d  43464  limsupmnflem  43511  limsupre3uzlem  43526  liminflelimsuplem  43566  xlimpnfxnegmnf  43605  xlimxrre  43622  xlimmnfvlem1  43623  xlimmnfv  43625  xlimpnfvlem1  43627  xlimpnfv  43629  climxlim2lem  43636  ioodvbdlimc1lem1  43722  ioodvbdlimc1lem2  43723  ioodvbdlimc2lem  43725  fourierdlem103  44000  fourierdlem104  44001  etransclem48  44073  saluncl  44108  subsaliuncllem  44146  sge0pnffigt  44185  omessle  44287  caragensplit  44289  omeunile  44294  hoidmvlelem2  44385  hoidmvlelem3  44386  hoidmvle  44389  vonvolmbllem  44449  vonvolmbl  44450  pimdecfgtioc  44504  smfpreimalt  44520  smfpreimaltf  44525  smfpreimale  44543  smfpreimagt  44551  smfpreimage  44571  smfmullem4  44583  smfinflem  44606  iccpartrn  45147  iccpartiun  45151  icceuelpart  45153  lidldomn1  45744  ply1mulgsumlem2  45993  lindslinindsimp2lem5  46068  lindslinindsimp2  46069  snlindsntor  46077  nn0sumshdiglemA  46230  nn0sumshdiglemB  46231  nn0sumshdig  46234