Theorem rspcva 3579

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is referenced by:  rexraleqim  3606  fsneq  7030  fvn0ssdmfun  7069  fveqdmss  7073  fvcofneq  7088  wfr3g  8312  boxriin  8934  boxcutc  8935  pwssfi  9157  marypha1lem  9389  supmo  9408  infmo  9453  unwdomg  9542  frr3g  9724  isinffi  9974  axdc3lem2  10430  grothac  10810  nqereu  10909  nnsub  12275  zextle  12664  xrsupsslem  13328  xrinfmsslem  13329  supxrunb1  13340  supxrunb2  13341  injresinjlem  13815  ssnn0fi  14017  suppssfz  14026  faclbnd4lem4  14328  ishashinf  14496  rexuz3  15396  cau3lem  15402  caubnd2  15405  o1co  15633  climcn1  15639  incexclem  15886  dvdsext  16374  mreintcl  17642  initoeu1  18063  initoeu2  18068  termoeu1  18070  lublecllem  18409  mgmidmo  18713  gsumval2  18739  dfgrp3lem  19099  symgfix2  19481  odeq  19615  gexid  19646  ringurd  20262  o2timesd  20287  rglcom4d  20288  gsummoncoe1  22468  m2detleiblem3  22786  m2detleiblem4  22787  cpmatmcllem  22875  mp2pm2mplem4  22966  cayleyhamilton1  23049  cmpsublem  23556  cmpsub  23557  cmpfii  23566  ptpjcn  23768  isufil2  24065  ufileu  24076  lmmbr  25417  caussi  25456  plyco0  26349  dgrco  26432  emcllem7  27166  isppw2  27279  addsrid  28157  mulsrid  28306  n0subs  28556  uvtxnbgrvtx  29743  rusgrnumwwlks  30326  clwwlkf  30398  vdgn1frgrv2  30647  frgrregorufr  30676  grpoidinvlem3  30858  grpoideu  30861  lnconi  32385  fsumiunle  33173  tpr2rico  34302  esumiun  34484  0elsiga  34504  sigaclci  34522  dya2icoseg2  34668  derangsn  35662  sat1el2xp  35871  fwddifnp1  36657  poimirlem25  38296  poimirlem26  38297  poimirlem30  38301  poimirlem31  38302  poimirlem32  38303  heicant  38306  mblfinlem2  38309  ftc1anc  38352  fdc  38396  bndss  38437  isdrngo2  38609  divrngidl  38679  maxidlmax  38694  cdleme0nex  41064  dihglblem2N  42068  hgmapvs  42665  ismrcd1  43429  nacsfg  43436  isnacs3  43441  nacsfix  43443  mzpcl1  43460  mzpcl2  43461  mzpcong  43699  dnnumch1  43771  aomclem1  43781  aomclem6  43786  lnr2i  43843  hbtlem5  43855  hbt  43857  rexanuz3  45814  choicefi  45917  suplesup  46055  xralrple2  46070  infxr  46082  infleinf  46087  xralrple4  46088  xralrple3  46089  xrralrecnnge  46105  supxrunb3  46114  supxrleubrnmpt  46120  unb2ltle  46129  suprleubrnmpt  46136  infxrgelbrnmpt  46168  supminfxr  46178  xrpnf  46199  islpcn  46353  limclner  46365  climd  46386  clim2d  46387  limsupmnflem  46434  limsupre3uzlem  46449  xlimpnfxnegmnf  46528  xlimxrre  46545  xlimmnfvlem1  46546  xlimmnfv  46548  xlimpnfvlem1  46550  xlimpnfv  46552  climxlim2lem  46559  ioodvbdlimc1lem1  46645  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  fourierdlem103  46923  fourierdlem104  46924  etransclem48  46996  saluncl  47031  subsaliuncllem  47071  sge0pnffigt  47110  omessle  47212  caragensplit  47214  omeunile  47219  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvle  47314  vonvolmbllem  47374  vonvolmbl  47375  pimdecfgtioc  47429  smfpreimalt  47445  smfpreimaltf  47450  smfpreimale  47468  smfpreimagt  47476  smfpreimage  47496  smfmullem4  47508  smfinflem  47531  iccpartrn  48179  iccpartiun  48183  icceuelpart  48185  lidldomn1  48996  ply1mulgsumlem2  49167  lindslinindsimp2lem5  49242  lindslinindsimp2  49243  snlindsntor  49251  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  nn0sumshdig  49403