Theorem rspcva 3604

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051

This theorem is referenced by:  rexraleqim  3630  fvn0ssdmfun  7083  fveqdmss  7087  fvcofneq  7102  wfr3g  8328  boxriin  8959  boxcutc  8960  marypha1lem  9463  supmo  9482  infmo  9525  unwdomg  9614  frr3g  9786  isinffi  10022  axdc3lem2  10481  grothac  10860  nqereu  10959  nnsub  12294  zextle  12673  xrsupsslem  13326  xrinfmsslem  13327  supxrunb1  13338  supxrunb2  13339  injresinjlem  13793  ssnn0fi  13991  suppssfz  14000  faclbnd4lem4  14299  ishashinf  14468  rexuz3  15339  cau3lem  15345  caubnd2  15348  o1co  15574  climcn1  15580  incexclem  15826  dvdsext  16309  mreintcl  17594  initoeu1  18019  initoeu2  18024  termoeu1  18026  lublecllem  18371  mgmidmo  18639  gsumval2  18665  dfgrp3lem  19018  symgfix2  19400  odeq  19534  gexid  19565  ringurd  20154  o2timesd  20179  rglcom4d  20180  gsummoncoe1  22269  m2detleiblem3  22592  m2detleiblem4  22593  cpmatmcllem  22681  mp2pm2mplem4  22772  cayleyhamilton1  22855  cmpsublem  23364  cmpsub  23365  cmpfii  23374  ptpjcn  23576  isufil2  23873  ufileu  23884  lmmbr  25247  caussi  25286  plyco0  26188  dgrco  26272  emcllem7  26999  isppw2  27112  addsrid  27947  mulsrid  28083  n0subs  28295  uvtxnbgrvtx  29298  rusgrnumwwlks  29877  clwwlkf  29949  vdgn1frgrv2  30198  frgrregorufr  30227  grpoidinvlem3  30408  grpoideu  30411  lnconi  31935  fsumiunle  32698  tpr2rico  33664  esumiun  33864  0elsiga  33884  sigaclci  33902  dya2icoseg2  34049  derangsn  34931  sat1el2xp  35140  fwddifnp1  35912  poimirlem25  37269  poimirlem26  37270  poimirlem30  37274  poimirlem31  37275  poimirlem32  37276  heicant  37279  mblfinlem2  37282  ftc1anc  37325  fdc  37369  bndss  37410  isdrngo2  37582  divrngidl  37652  maxidlmax  37667  cdleme0nex  39913  dihglblem2N  40917  hgmapvs  41514  ismrcd1  42265  nacsfg  42272  isnacs3  42277  nacsfix  42279  mzpcl1  42296  mzpcl2  42297  mzpcong  42540  dnnumch1  42615  aomclem1  42625  aomclem6  42630  lnr2i  42687  hbtlem5  42699  hbt  42701  pwssfi  44556  rexanuz3  44607  choicefi  44717  fsneq  44723  suplesup  44864  xralrple2  44879  infxr  44892  infleinf  44897  xralrple4  44898  xralrple3  44899  xrralrecnnge  44915  supxrunb3  44924  supxrleubrnmpt  44931  unb2ltle  44940  suprleubrnmpt  44947  infxrgelbrnmpt  44979  supminfxr  44989  xrpnf  45011  islpcn  45170  limclner  45182  climd  45203  clim2d  45204  limsupmnflem  45251  limsupre3uzlem  45266  liminflelimsuplem  45306  xlimpnfxnegmnf  45345  xlimxrre  45362  xlimmnfvlem1  45363  xlimmnfv  45365  xlimpnfvlem1  45367  xlimpnfv  45369  climxlim2lem  45376  ioodvbdlimc1lem1  45462  ioodvbdlimc1lem2  45463  ioodvbdlimc2lem  45465  fourierdlem103  45740  fourierdlem104  45741  etransclem48  45813  saluncl  45848  subsaliuncllem  45888  sge0pnffigt  45927  omessle  46029  caragensplit  46031  omeunile  46036  hoidmvlelem2  46127  hoidmvlelem3  46128  hoidmvle  46131  vonvolmbllem  46191  vonvolmbl  46192  pimdecfgtioc  46246  smfpreimalt  46262  smfpreimaltf  46267  smfpreimale  46285  smfpreimagt  46293  smfpreimage  46313  smfmullem4  46325  smfinflem  46348  iccpartrn  46912  iccpartiun  46916  icceuelpart  46918  lidldomn1  47484  ply1mulgsumlem2  47646  lindslinindsimp2lem5  47721  lindslinindsimp2  47722  snlindsntor  47730  nn0sumshdiglemA  47883  nn0sumshdiglemB  47884  nn0sumshdig  47887