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  27876  mulsrid  28021  n0subs  28258  uvtxnbgrvtx  29338  rusgrnumwwlks  29919  clwwlkf  29991  vdgn1frgrv2  30240  frgrregorufr  30269  grpoidinvlem3  30450  grpoideu  30453  lnconi  31977  fsumiunle  32774  tpr2rico  33879  esumiun  34061  0elsiga  34081  sigaclci  34099  dya2icoseg2  34246  derangsn  35147  sat1el2xp  35356  fwddifnp1  36143  poimirlem25  37629  poimirlem26  37630  poimirlem30  37634  poimirlem31  37635  poimirlem32  37636  heicant  37639  mblfinlem2  37642  ftc1anc  37685  fdc  37729  bndss  37770  isdrngo2  37942  divrngidl  38012  maxidlmax  38027  cdleme0nex  40273  dihglblem2N  41277  hgmapvs  41874  ismrcd1  42675  nacsfg  42682  isnacs3  42687  nacsfix  42689  mzpcl1  42706  mzpcl2  42707  mzpcong  42949  dnnumch1  43021  aomclem1  43031  aomclem6  43036  lnr2i  43093  hbtlem5  43105  hbt  43107  rexanuz3  45078  choicefi  45182  fsneq  45188  suplesup  45323  xralrple2  45338  infxr  45350  infleinf  45355  xralrple4  45356  xralrple3  45357  xrralrecnnge  45373  supxrunb3  45382  supxrleubrnmpt  45389  unb2ltle  45398  suprleubrnmpt  45405  infxrgelbrnmpt  45437  supminfxr  45447  xrpnf  45468  islpcn  45624  limclner  45636  climd  45657  clim2d  45658  limsupmnflem  45705  limsupre3uzlem  45720  xlimpnfxnegmnf  45799  xlimxrre  45816  xlimmnfvlem1  45817  xlimmnfv  45819  xlimpnfvlem1  45821  xlimpnfv  45823  climxlim2lem  45830  ioodvbdlimc1lem1  45916  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  fourierdlem103  46194  fourierdlem104  46195  etransclem48  46267  saluncl  46302  subsaliuncllem  46342  sge0pnffigt  46381  omessle  46483  caragensplit  46485  omeunile  46490  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvle  46585  vonvolmbllem  46645  vonvolmbl  46646  pimdecfgtioc  46700  smfpreimalt  46716  smfpreimaltf  46721  smfpreimale  46739  smfpreimagt  46747  smfpreimage  46767  smfmullem4  46779  smfinflem  46802  iccpartrn  47418  iccpartiun  47422  icceuelpart  47424  lidldomn1  48219  ply1mulgsumlem2  48376  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  snlindsntor  48460  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdig  48612