Theorem rspcva 3582

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3082

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083

This theorem is used by:  rexraleqim  3609  fsneq  7037  fvn0ssdmfun  7076  fveqdmss  7080  fvcofneq  7095  wfr3g  8325  boxriin  8947  boxcutc  8948  pwssfi  9171  marypha1lem  9403  supmo  9422  infmo  9467  unwdomg  9556  frr3g  9738  isinffi  9997  axdc3lem2  10453  grothac  10833  nqereu  10932  nnsub  12298  zextle  12687  xrsupsslem  13351  xrinfmsslem  13352  supxrunb1  13363  supxrunb2  13364  injresinjlem  13838  ssnn0fi  14041  suppssfz  14050  faclbnd4lem4  14352  ishashinf  14520  rexuz3  15426  cau3lem  15432  caubnd2  15435  o1co  15663  climcn1  15669  incexclem  15916  dvdsext  16404  mreintcl  17672  initoeu1  18093  initoeu2  18098  termoeu1  18100  lublecllem  18439  mgmidmo  18743  gsumval2  18769  dfgrp3lem  19129  symgfix2  19511  odeq  19645  gexid  19676  ringurd  20292  o2timesd  20317  rglcom4d  20318  gsummoncoe1  22498  m2detleiblem3  22816  m2detleiblem4  22817  cpmatmcllem  22905  mp2pm2mplem4  22996  cayleyhamilton1  23079  cmpsublem  23586  cmpsub  23587  cmpfii  23596  ptpjcn  23798  isufil2  24095  ufileu  24106  lmmbr  25447  caussi  25486  plyco0  26379  dgrco  26462  emcllem7  27196  isppw2  27309  addsrid  28187  mulsrid  28336  n0subs  28586  uvtxnbgrvtx  29773  rusgrnumwwlks  30356  clwwlkf  30428  vdgn1frgrv2  30677  frgrregorufr  30706  grpoidinvlem3  30888  grpoideu  30891  lnconi  32415  fsumiunle  33203  tpr2rico  34326  esumiun  34508  0elsiga  34528  sigaclci  34546  dya2icoseg2  34692  derangsn  35675  sat1el2xp  35884  fwddifnp1  36670  poimirlem25  38329  poimirlem26  38330  poimirlem30  38334  poimirlem31  38335  poimirlem32  38336  heicant  38339  mblfinlem2  38342  ftc1anc  38385  fdc  38429  bndss  38470  isdrngo2  38642  divrngidl  38712  maxidlmax  38727  cdleme0nex  41097  dihglblem2N  42101  hgmapvs  42698  ismrcd1  43462  nacsfg  43469  isnacs3  43474  nacsfix  43476  mzpcl1  43493  mzpcl2  43494  mzpcong  43732  dnnumch1  43804  aomclem1  43814  aomclem6  43819  lnr2i  43876  hbtlem5  43888  hbt  43890  rexanuz3  45847  choicefi  45950  suplesup  46088  xralrple2  46103  infxr  46115  infleinf  46120  xralrple4  46121  xralrple3  46122  xrralrecnnge  46138  supxrunb3  46147  supxrleubrnmpt  46153  unb2ltle  46162  suprleubrnmpt  46169  infxrgelbrnmpt  46201  supminfxr  46211  xrpnf  46232  islpcn  46386  limclner  46398  climd  46419  clim2d  46420  limsupmnflem  46467  limsupre3uzlem  46482  xlimpnfxnegmnf  46561  xlimxrre  46578  xlimmnfvlem1  46579  xlimmnfv  46581  xlimpnfvlem1  46583  xlimpnfv  46585  climxlim2lem  46592  ioodvbdlimc1lem1  46678  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  fourierdlem103  46956  fourierdlem104  46957  etransclem48  47029  saluncl  47064  subsaliuncllem  47104  sge0pnffigt  47143  omessle  47245  caragensplit  47247  omeunile  47252  hoidmvlelem2  47343  hoidmvlelem3  47344  hoidmvle  47347  vonvolmbllem  47407  vonvolmbl  47408  pimdecfgtioc  47462  smfpreimalt  47478  smfpreimaltf  47483  smfpreimale  47501  smfpreimagt  47509  smfpreimage  47529  smfmullem4  47541  smfinflem  47564  iccpartrn  48212  iccpartiun  48216  icceuelpart  48218  lidldomn1  49029  ply1mulgsumlem2  49200  lindslinindsimp2lem5  49275  lindslinindsimp2  49276  snlindsntor  49284  nn0sumshdiglemA  49432  nn0sumshdiglemB  49433  nn0sumshdig  49436