Theorem rspcva 3611

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  rexraleqim  3636  fvn0ssdmfun  7077  fveqdmss  7081  fvcofneq  7095  wfr3g  8307  boxriin  8934  boxcutc  8935  marypha1lem  9428  supmo  9447  infmo  9490  unwdomg  9579  frr3g  9751  isinffi  9987  axdc3lem2  10446  grothac  10825  nqereu  10924  nnsub  12256  zextle  12635  xrsupsslem  13286  xrinfmsslem  13287  supxrunb1  13298  supxrunb2  13299  injresinjlem  13752  ssnn0fi  13950  suppssfz  13959  faclbnd4lem4  14256  ishashinf  14424  rexuz3  15295  cau3lem  15301  caubnd2  15304  o1co  15530  climcn1  15536  incexclem  15782  dvdsext  16264  mreintcl  17539  initoeu1  17961  initoeu2  17966  termoeu1  17968  lublecllem  18313  mgmidmo  18579  gsumval2  18605  dfgrp3lem  18921  symgfix2  19284  odeq  19418  gexid  19449  ringurd  20008  o2timesd  20033  rglcom4d  20034  gsummoncoe1  21828  m2detleiblem3  22131  m2detleiblem4  22132  cpmatmcllem  22220  mp2pm2mplem4  22311  cayleyhamilton1  22394  cmpsublem  22903  cmpsub  22904  cmpfii  22913  ptpjcn  23115  isufil2  23412  ufileu  23423  lmmbr  24775  caussi  24814  plyco0  25706  dgrco  25789  emcllem7  26506  isppw2  26619  addsrid  27450  mulsrid  27572  uvtxnbgrvtx  28681  rusgrnumwwlks  29259  clwwlkf  29331  vdgn1frgrv2  29580  frgrregorufr  29609  grpoidinvlem3  29790  grpoideu  29793  lnconi  31317  fsumiunle  32066  tpr2rico  32923  esumiun  33123  0elsiga  33143  sigaclci  33161  dya2icoseg2  33308  derangsn  34192  sat1el2xp  34401  fwddifnp1  35168  poimirlem25  36561  poimirlem26  36562  poimirlem30  36566  poimirlem31  36567  poimirlem32  36568  heicant  36571  mblfinlem2  36574  ftc1anc  36617  fdc  36661  bndss  36702  isdrngo2  36874  divrngidl  36944  maxidlmax  36959  cdleme0nex  39209  dihglblem2N  40213  hgmapvs  40810  ismrcd1  41484  nacsfg  41491  isnacs3  41496  nacsfix  41498  mzpcl1  41515  mzpcl2  41516  mzpcong  41759  dnnumch1  41834  aomclem1  41844  aomclem6  41849  lnr2i  41906  hbtlem5  41918  hbt  41920  pwssfi  43780  rexanuz3  43833  choicefi  43947  fsneq  43953  suplesup  44097  xralrple2  44112  infxr  44125  infleinf  44130  xralrple4  44131  xralrple3  44132  xrralrecnnge  44148  supxrunb3  44157  supxrleubrnmpt  44164  unb2ltle  44173  suprleubrnmpt  44180  infxrgelbrnmpt  44212  supminfxr  44222  xrpnf  44244  islpcn  44403  limclner  44415  climd  44436  clim2d  44437  limsupmnflem  44484  limsupre3uzlem  44499  liminflelimsuplem  44539  xlimpnfxnegmnf  44578  xlimxrre  44595  xlimmnfvlem1  44596  xlimmnfv  44598  xlimpnfvlem1  44600  xlimpnfv  44602  climxlim2lem  44609  ioodvbdlimc1lem1  44695  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  fourierdlem103  44973  fourierdlem104  44974  etransclem48  45046  saluncl  45081  subsaliuncllem  45121  sge0pnffigt  45160  omessle  45262  caragensplit  45264  omeunile  45269  hoidmvlelem2  45360  hoidmvlelem3  45361  hoidmvle  45364  vonvolmbllem  45424  vonvolmbl  45425  pimdecfgtioc  45479  smfpreimalt  45495  smfpreimaltf  45500  smfpreimale  45518  smfpreimagt  45526  smfpreimage  45546  smfmullem4  45558  smfinflem  45581  iccpartrn  46146  iccpartiun  46150  icceuelpart  46152  lidldomn1  46871  ply1mulgsumlem2  47116  lindslinindsimp2lem5  47191  lindslinindsimp2  47192  snlindsntor  47200  nn0sumshdiglemA  47353  nn0sumshdiglemB  47354  nn0sumshdig  47357