Theorem rspcva 3619

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059

This theorem is referenced by:  rexraleqim  3646  fvn0ssdmfun  7093  fveqdmss  7097  fvcofneq  7112  wfr3g  8345  boxriin  8978  boxcutc  8979  marypha1lem  9470  supmo  9489  infmo  9532  unwdomg  9621  frr3g  9793  isinffi  10029  axdc3lem2  10488  grothac  10867  nqereu  10966  nnsub  12307  zextle  12688  xrsupsslem  13345  xrinfmsslem  13346  supxrunb1  13357  supxrunb2  13358  injresinjlem  13822  ssnn0fi  14022  suppssfz  14031  faclbnd4lem4  14331  ishashinf  14498  rexuz3  15383  cau3lem  15389  caubnd2  15392  o1co  15618  climcn1  15624  incexclem  15868  dvdsext  16354  mreintcl  17639  initoeu1  18064  initoeu2  18069  termoeu1  18071  lublecllem  18417  mgmidmo  18685  gsumval2  18711  dfgrp3lem  19068  symgfix2  19448  odeq  19582  gexid  19613  ringurd  20202  o2timesd  20227  rglcom4d  20228  gsummoncoe1  22327  m2detleiblem3  22650  m2detleiblem4  22651  cpmatmcllem  22739  mp2pm2mplem4  22830  cayleyhamilton1  22913  cmpsublem  23422  cmpsub  23423  cmpfii  23432  ptpjcn  23634  isufil2  23931  ufileu  23942  lmmbr  25305  caussi  25344  plyco0  26245  dgrco  26329  emcllem7  27059  isppw2  27172  addsrid  28011  mulsrid  28153  n0subs  28374  uvtxnbgrvtx  29424  rusgrnumwwlks  30003  clwwlkf  30075  vdgn1frgrv2  30324  frgrregorufr  30353  grpoidinvlem3  30534  grpoideu  30537  lnconi  32061  fsumiunle  32835  tpr2rico  33872  esumiun  34074  0elsiga  34094  sigaclci  34112  dya2icoseg2  34259  derangsn  35154  sat1el2xp  35363  fwddifnp1  36146  poimirlem25  37631  poimirlem26  37632  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  heicant  37641  mblfinlem2  37644  ftc1anc  37687  fdc  37731  bndss  37772  isdrngo2  37944  divrngidl  38014  maxidlmax  38029  cdleme0nex  40272  dihglblem2N  41276  hgmapvs  41873  ismrcd1  42685  nacsfg  42692  isnacs3  42697  nacsfix  42699  mzpcl1  42716  mzpcl2  42717  mzpcong  42960  dnnumch1  43032  aomclem1  43042  aomclem6  43047  lnr2i  43104  hbtlem5  43116  hbt  43118  pwssfi  44984  rexanuz3  45035  choicefi  45142  fsneq  45148  suplesup  45288  xralrple2  45303  infxr  45316  infleinf  45321  xralrple4  45322  xralrple3  45323  xrralrecnnge  45339  supxrunb3  45348  supxrleubrnmpt  45355  unb2ltle  45364  suprleubrnmpt  45371  infxrgelbrnmpt  45403  supminfxr  45413  xrpnf  45435  islpcn  45594  limclner  45606  climd  45627  clim2d  45628  limsupmnflem  45675  limsupre3uzlem  45690  liminflelimsuplem  45730  xlimpnfxnegmnf  45769  xlimxrre  45786  xlimmnfvlem1  45787  xlimmnfv  45789  xlimpnfvlem1  45791  xlimpnfv  45793  climxlim2lem  45800  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  fourierdlem103  46164  fourierdlem104  46165  etransclem48  46237  saluncl  46272  subsaliuncllem  46312  sge0pnffigt  46351  omessle  46453  caragensplit  46455  omeunile  46460  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvle  46555  vonvolmbllem  46615  vonvolmbl  46616  pimdecfgtioc  46670  smfpreimalt  46686  smfpreimaltf  46691  smfpreimale  46709  smfpreimagt  46717  smfpreimage  46737  smfmullem4  46749  smfinflem  46772  iccpartrn  47354  iccpartiun  47358  icceuelpart  47360  lidldomn1  48074  ply1mulgsumlem2  48232  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  snlindsntor  48316  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdig  48472