Theorem rspcva 3574

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rexraleqim  3601  fvn0ssdmfun  7019  fveqdmss  7023  fvcofneq  7038  wfr3g  8261  boxriin  8878  boxcutc  8879  pwssfi  9101  marypha1lem  9336  supmo  9355  infmo  9400  unwdomg  9489  frr3g  9668  isinffi  9904  axdc3lem2  10361  grothac  10741  nqereu  10840  nnsub  12189  zextle  12565  xrsupsslem  13222  xrinfmsslem  13223  supxrunb1  13234  supxrunb2  13235  injresinjlem  13706  ssnn0fi  13908  suppssfz  13917  faclbnd4lem4  14219  ishashinf  14386  rexuz3  15272  cau3lem  15278  caubnd2  15281  o1co  15509  climcn1  15515  incexclem  15759  dvdsext  16248  mreintcl  17514  initoeu1  17935  initoeu2  17940  termoeu1  17942  lublecllem  18281  mgmidmo  18585  gsumval2  18611  dfgrp3lem  18968  symgfix2  19345  odeq  19479  gexid  19510  ringurd  20120  o2timesd  20145  rglcom4d  20146  gsummoncoe1  22252  m2detleiblem3  22573  m2detleiblem4  22574  cpmatmcllem  22662  mp2pm2mplem4  22753  cayleyhamilton1  22836  cmpsublem  23343  cmpsub  23344  cmpfii  23353  ptpjcn  23555  isufil2  23852  ufileu  23863  lmmbr  25214  caussi  25253  plyco0  26153  dgrco  26237  emcllem7  26968  isppw2  27081  addsrid  27960  mulsrid  28109  n0subs  28359  uvtxnbgrvtx  29466  rusgrnumwwlks  30050  clwwlkf  30122  vdgn1frgrv2  30371  frgrregorufr  30400  grpoidinvlem3  30581  grpoideu  30584  lnconi  32108  fsumiunle  32910  tpr2rico  34069  esumiun  34251  0elsiga  34271  sigaclci  34289  dya2icoseg2  34435  derangsn  35364  sat1el2xp  35573  fwddifnp1  36359  poimirlem25  37846  poimirlem26  37847  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  heicant  37856  mblfinlem2  37859  ftc1anc  37902  fdc  37946  bndss  37987  isdrngo2  38159  divrngidl  38229  maxidlmax  38244  cdleme0nex  40550  dihglblem2N  41554  hgmapvs  42151  ismrcd1  42940  nacsfg  42947  isnacs3  42952  nacsfix  42954  mzpcl1  42971  mzpcl2  42972  mzpcong  43214  dnnumch1  43286  aomclem1  43296  aomclem6  43301  lnr2i  43358  hbtlem5  43370  hbt  43372  rexanuz3  45340  choicefi  45444  fsneq  45450  suplesup  45584  xralrple2  45599  infxr  45611  infleinf  45616  xralrple4  45617  xralrple3  45618  xrralrecnnge  45634  supxrunb3  45643  supxrleubrnmpt  45650  unb2ltle  45659  suprleubrnmpt  45666  infxrgelbrnmpt  45698  supminfxr  45708  xrpnf  45729  islpcn  45883  limclner  45895  climd  45916  clim2d  45917  limsupmnflem  45964  limsupre3uzlem  45979  xlimpnfxnegmnf  46058  xlimxrre  46075  xlimmnfvlem1  46076  xlimmnfv  46078  xlimpnfvlem1  46080  xlimpnfv  46082  climxlim2lem  46089  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  fourierdlem103  46453  fourierdlem104  46454  etransclem48  46526  saluncl  46561  subsaliuncllem  46601  sge0pnffigt  46640  omessle  46742  caragensplit  46744  omeunile  46749  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvle  46844  vonvolmbllem  46904  vonvolmbl  46905  pimdecfgtioc  46959  smfpreimalt  46975  smfpreimaltf  46980  smfpreimale  46998  smfpreimagt  47006  smfpreimage  47026  smfmullem4  47038  smfinflem  47061  iccpartrn  47676  iccpartiun  47680  icceuelpart  47682  lidldomn1  48477  ply1mulgsumlem2  48633  lindslinindsimp2lem5  48708  lindslinindsimp2  48709  snlindsntor  48717  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  nn0sumshdig  48869