Theorem rspcva 3496

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2155  ∀wral 3092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-v 3389

This theorem is referenced by:  rexraleqim  3518  fvn0ssdmfun  6566  fveqdmss  6570  fvcofneq  6583  wfr3g  7642  boxriin  8181  boxcutc  8182  marypha1lem  8572  supmo  8591  infmo  8634  unwdomg  8722  isinffi  9095  axdc3lem2  9552  grothac  9931  nqereu  10030  nnsub  11339  zextle  11710  xrsupsslem  12349  xrinfmsslem  12350  supxrunb1  12361  supxrunb2  12362  injresinjlem  12806  ssnn0fi  13002  suppssfz  13011  faclbnd4lem4  13297  ishashinf  13458  rexuz3  14305  cau3lem  14311  caubnd2  14314  o1co  14534  climcn1  14539  incexclem  14784  dvdsext  15260  mreintcl  16454  initoeu1  16859  initoeu2  16864  termoeu1  16866  lublecllem  17187  mgmidmo  17458  gsumval2  17479  dfgrp3lem  17712  symgfix2  18031  odeq  18164  gexid  18191  gsummoncoe1  19876  m2detleiblem3  20640  m2detleiblem4  20641  cpmatmcllem  20730  mp2pm2mplem4  20821  cayleyhamilton1  20904  cmpsublem  21410  cmpsub  21411  cmpfii  21420  ptpjcn  21622  isufil2  21919  ufileu  21930  lmmbr  23262  caussi  23301  plyco0  24156  dgrco  24239  emcllem7  24936  isppw2  25049  uvtxnbgrvtx  26507  rusgrnumwwlks  27110  clwwlkf  27190  eupthseg  27373  upgreupthseg  27376  vdgn1frgrv2  27465  frgrregorufr  27494  extwwlkfablem1OLD  27511  grpoidinvlem3  27683  grpoideu  27686  lnconi  29214  fsumiunle  29896  rngurd  30107  tpr2rico  30277  esumiun  30475  ofcfeqd2  30482  0elsiga  30496  sigaclci  30514  dya2icoseg2  30659  signstfvneq0  30968  derangsn  31469  frr3g  32094  fwddifnp1  32587  poimirlem25  33741  poimirlem26  33742  poimirlem30  33746  poimirlem31  33747  poimirlem32  33748  heicant  33751  mblfinlem2  33754  ftc1anc  33799  fdc  33846  bndss  33890  isdrngo2  34062  divrngidl  34132  maxidlmax  34147  cdleme0nex  36065  dihglblem2N  37069  hgmapvs  37666  ismrcd1  37757  nacsfg  37764  isnacs3  37769  nacsfix  37771  mzpcl1  37788  mzpcl2  37789  mzpcong  38034  dnnumch1  38109  fnwe2lem2  38116  aomclem1  38119  aomclem4  38122  aomclem6  38124  lnr2i  38181  hbtlem5  38193  hbt  38195  pwssfi  39698  eliind  39727  rexanuz3  39762  choicefi  39873  fsneq  39879  rnmptbd2lem  39940  rnmptbdlem  39947  suplesup  40029  xralrple2  40044  infxr  40057  infleinf  40062  xralrple4  40063  xralrple3  40064  xrralrecnnge  40086  supxrunb3  40096  supxrleubrnmpt  40105  unb2ltle  40115  suprleubrnmpt  40122  infxrgelbrnmpt  40156  supminfxr  40167  xrpnf  40189  islpcn  40345  limclner  40357  climd  40378  clim2d  40379  limsupmnflem  40426  limsupre3uzlem  40441  liminflelimsuplem  40481  xlimxrre  40531  xlimmnfvlem1  40532  xlimmnfv  40534  xlimpnfvlem1  40536  xlimpnfv  40538  climxlim2lem  40545  ioodvbdlimc1lem1  40620  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  fourierdlem103  40899  fourierdlem104  40900  etransclem48  40972  salunicl  41009  saluncl  41010  subsaliuncllem  41048  sge0pnffigt  41086  meadjuni  41147  omessle  41188  caragensplit  41190  omeunile  41195  hoidmvlelem2  41286  hoidmvlelem3  41287  hoidmvle  41290  vonvolmbllem  41350  vonvolmbl  41351  pimdecfgtioc  41401  smfpreimalt  41416  smfpreimaltf  41421  smfpreimale  41439  smfpreimagt  41446  smfpreimage  41466  smfmullem4  41477  smfinflem  41499  iccpartimp  41922  iccpartrn  41935  iccpartiun  41939  icceuelpart  41941  reuccatpfxs1  42003  lidldomn1  42483  ply1mulgsumlem2  42737  lindslinindsimp2lem5  42813  lindslinindsimp2  42814  snlindsntor  42822  nn0sumshdiglemA  42975  nn0sumshdiglemB  42976  nn0sumshdig  42979