Theorem rspcva 3575

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 3573	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = 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:  rexraleqim  3602  fvn0ssdmfun  7008  fveqdmss  7012  fvcofneq  7027  wfr3g  8252  boxriin  8867  boxcutc  8868  pwssfi  9091  marypha1lem  9323  supmo  9342  infmo  9387  unwdomg  9476  frr3g  9652  isinffi  9888  axdc3lem2  10345  grothac  10724  nqereu  10823  nnsub  12172  zextle  12549  xrsupsslem  13209  xrinfmsslem  13210  supxrunb1  13221  supxrunb2  13222  injresinjlem  13690  ssnn0fi  13892  suppssfz  13901  faclbnd4lem4  14203  ishashinf  14370  rexuz3  15256  cau3lem  15262  caubnd2  15265  o1co  15493  climcn1  15499  incexclem  15743  dvdsext  16232  mreintcl  17497  initoeu1  17918  initoeu2  17923  termoeu1  17925  lublecllem  18264  mgmidmo  18534  gsumval2  18560  dfgrp3lem  18917  symgfix2  19295  odeq  19429  gexid  19460  ringurd  20070  o2timesd  20095  rglcom4d  20096  gsummoncoe1  22193  m2detleiblem3  22514  m2detleiblem4  22515  cpmatmcllem  22603  mp2pm2mplem4  22694  cayleyhamilton1  22777  cmpsublem  23284  cmpsub  23285  cmpfii  23294  ptpjcn  23496  isufil2  23793  ufileu  23804  lmmbr  25156  caussi  25195  plyco0  26095  dgrco  26179  emcllem7  26910  isppw2  27023  addsrid  27878  mulsrid  28023  n0subs  28260  uvtxnbgrvtx  29342  rusgrnumwwlks  29923  clwwlkf  29995  vdgn1frgrv2  30244  frgrregorufr  30273  grpoidinvlem3  30454  grpoideu  30457  lnconi  31981  fsumiunle  32783  tpr2rico  33895  esumiun  34077  0elsiga  34097  sigaclci  34115  dya2icoseg2  34262  derangsn  35163  sat1el2xp  35372  fwddifnp1  36159  poimirlem25  37645  poimirlem26  37646  poimirlem30  37650  poimirlem31  37651  poimirlem32  37652  heicant  37655  mblfinlem2  37658  ftc1anc  37701  fdc  37745  bndss  37786  isdrngo2  37958  divrngidl  38028  maxidlmax  38043  cdleme0nex  40289  dihglblem2N  41293  hgmapvs  41890  ismrcd1  42691  nacsfg  42698  isnacs3  42703  nacsfix  42705  mzpcl1  42722  mzpcl2  42723  mzpcong  42965  dnnumch1  43037  aomclem1  43047  aomclem6  43052  lnr2i  43109  hbtlem5  43121  hbt  43123  rexanuz3  45094  choicefi  45198  fsneq  45204  suplesup  45339  xralrple2  45354  infxr  45366  infleinf  45371  xralrple4  45372  xralrple3  45373  xrralrecnnge  45389  supxrunb3  45398  supxrleubrnmpt  45405  unb2ltle  45414  suprleubrnmpt  45421  infxrgelbrnmpt  45453  supminfxr  45463  xrpnf  45484  islpcn  45640  limclner  45652  climd  45673  clim2d  45674  limsupmnflem  45721  limsupre3uzlem  45736  xlimpnfxnegmnf  45815  xlimxrre  45832  xlimmnfvlem1  45833  xlimmnfv  45835  xlimpnfvlem1  45837  xlimpnfv  45839  climxlim2lem  45846  ioodvbdlimc1lem1  45932  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  fourierdlem103  46210  fourierdlem104  46211  etransclem48  46283  saluncl  46318  subsaliuncllem  46358  sge0pnffigt  46397  omessle  46499  caragensplit  46501  omeunile  46506  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvle  46601  vonvolmbllem  46661  vonvolmbl  46662  pimdecfgtioc  46716  smfpreimalt  46732  smfpreimaltf  46737  smfpreimale  46755  smfpreimagt  46763  smfpreimage  46783  smfmullem4  46795  smfinflem  46818  iccpartrn  47434  iccpartiun  47438  icceuelpart  47440  lidldomn1  48235  ply1mulgsumlem2  48392  lindslinindsimp2lem5  48467  lindslinindsimp2  48468  snlindsntor  48476  nn0sumshdiglemA  48624  nn0sumshdiglemB  48625  nn0sumshdig  48628