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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rexraleqim  3600  fsneq  7039  fvn0ssdmfun  7079  fveqdmss  7083  fvcofneq  7098  wfr3g  8345  boxriin  8976  boxcutc  8977  pwssfi  9200  marypha1lem  9432  supmo  9451  infmo  9496  unwdomg  9585  frr3g  9767  hfelhf  9921  isinffi  10080  axdc3lem2  10536  grothac  10922  nqereu  11021  nnsub  12389  zextle  12779  xrsupsslem  13444  xrinfmsslem  13445  supxrunb1  13456  supxrunb2  13457  injresinjlem  13932  ssnn0fi  14135  suppssfz  14144  faclbnd4lem4  14447  ishashinf  14615  rexuz3  15525  cau3lem  15531  caubnd2  15534  o1co  15762  climcn1  15768  incexclem  16014  dvdsext  16500  mreintcl  17774  initoeu1  18195  initoeu2  18200  termoeu1  18202  lublecllem  18541  mgmidmo  18847  gsumval2  18884  dfgrp3lem  19257  symgfix2  19639  odeq  19773  gexid  19804  ringurd  20420  o2timesd  20445  rglcom4d  20446  gsummoncoe1  22635  m2detleiblem3  22953  m2detleiblem4  22954  cpmatmcllem  23045  mp2pm2mplem4  23136  cayleyhamilton1  23219  cmpsublem  23726  cmpsub  23727  cmpfii  23736  ptpjcn  23939  isufil2  24236  ufileu  24247  lmmbr  25588  caussi  25627  plyco0  26519  dgrco  26603  emcllem7  27338  isppw2  27451  addsrid  28359  mulsrid  28508  n0subs  28758  uvtxnbgrvtx  29983  rusgrnumwwlks  30575  clwwlkf  30647  vdgn1frgrv2  30906  frgrregorufr  30935  grpoidinvlem3  31117  grpoideu  31120  lnconi  32644  fsumiunle  33470  tpr2rico  34594  esumiun  34776  0elsiga  34796  sigaclci  34814  dya2icoseg2  34960  derangsn  36053  sat1el2xp  36262  fwddifnp1  37054  poimirlem25  38700  poimirlem26  38701  poimirlem30  38705  poimirlem31  38706  poimirlem32  38707  heicant  38710  mblfinlem2  38713  ftc1anc  38756  fdc  38816  bndss  38857  isdrngo2  39029  divrngidl  39099  maxidlmax  39114  cdleme0nex  41484  dihglblem2N  42488  hgmapvs  43085  ismrcd1  43846  nacsfg  43853  isnacs3  43858  nacsfix  43860  mzpcl1  43877  mzpcl2  43878  mzpcong  44116  dnnumch1  44188  aomclem1  44193  aomclem6  44198  lnr2i  44255  hbtlem5  44267  hbt  44269  rexanuz3  46247  choicefi  46350  suplesup  46487  xralrple2  46502  infxr  46514  infleinf  46519  xralrple4  46520  xralrple3  46521  xrralrecnnge  46537  supxrunb3  46546  supxrleubrnmpt  46552  unb2ltle  46561  suprleubrnmpt  46568  infxrgelbrnmpt  46600  supminfxr  46610  xrpnf  46631  islpcn  46785  limclner  46797  climd  46818  clim2d  46819  limsupmnflem  46866  limsupre3uzlem  46881  xlimpnfxnegmnf  46960  xlimxrre  46977  xlimmnfvlem1  46978  xlimmnfv  46980  xlimpnfvlem1  46982  xlimpnfv  46984  climxlim2lem  46991  ioodvbdlimc1lem1  47077  ioodvbdlimc1lem2  47078  ioodvbdlimc2lem  47080  fourierdlem103  47355  fourierdlem104  47356  etransclem48  47428  saluncl  47463  subsaliuncllem  47503  sge0pnffigt  47542  omessle  47644  caragensplit  47646  omeunile  47651  hoidmvlelem2  47742  hoidmvlelem3  47743  hoidmvle  47746  vonvolmbllem  47806  vonvolmbl  47807  pimdecfgtioc  47861  smfpreimalt  47877  smfpreimaltf  47882  smfpreimale  47900  smfpreimagt  47908  smfpreimage  47928  smfmullem4  47940  smfinflem  47963  iccpartrn  48648  iccpartiun  48652  icceuelpart  48654  lidldomn1  49464  ply1mulgsumlem2  49635  lindslinindsimp2lem5  49710  lindslinindsimp2  49711  snlindsntor  49719  nn0sumshdiglemA  49867  nn0sumshdiglemB  49868  nn0sumshdig  49871