Theorem rspcva 3563

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rexraleqim  3590  fvn0ssdmfun  7021  fveqdmss  7025  fvcofneq  7040  wfr3g  8263  boxriin  8882  boxcutc  8883  pwssfi  9105  marypha1lem  9340  supmo  9359  infmo  9404  unwdomg  9493  frr3g  9674  isinffi  9910  axdc3lem2  10367  grothac  10747  nqereu  10846  nnsub  12215  zextle  12596  xrsupsslem  13253  xrinfmsslem  13254  supxrunb1  13265  supxrunb2  13266  injresinjlem  13739  ssnn0fi  13941  suppssfz  13950  faclbnd4lem4  14252  ishashinf  14419  rexuz3  15305  cau3lem  15311  caubnd2  15314  o1co  15542  climcn1  15548  incexclem  15795  dvdsext  16284  mreintcl  17551  initoeu1  17972  initoeu2  17977  termoeu1  17979  lublecllem  18318  mgmidmo  18622  gsumval2  18648  dfgrp3lem  19008  symgfix2  19385  odeq  19519  gexid  19550  ringurd  20160  o2timesd  20185  rglcom4d  20186  gsummoncoe1  22286  m2detleiblem3  22607  m2detleiblem4  22608  cpmatmcllem  22696  mp2pm2mplem4  22787  cayleyhamilton1  22870  cmpsublem  23377  cmpsub  23378  cmpfii  23387  ptpjcn  23589  isufil2  23886  ufileu  23897  lmmbr  25238  caussi  25277  plyco0  26170  dgrco  26253  emcllem7  26982  isppw2  27095  addsrid  27973  mulsrid  28122  n0subs  28372  uvtxnbgrvtx  29479  rusgrnumwwlks  30063  clwwlkf  30135  vdgn1frgrv2  30384  frgrregorufr  30413  grpoidinvlem3  30595  grpoideu  30598  lnconi  32122  fsumiunle  32920  tpr2rico  34075  esumiun  34257  0elsiga  34277  sigaclci  34295  dya2icoseg2  34441  derangsn  35371  sat1el2xp  35580  fwddifnp1  36366  poimirlem25  37983  poimirlem26  37984  poimirlem30  37988  poimirlem31  37989  poimirlem32  37990  heicant  37993  mblfinlem2  37996  ftc1anc  38039  fdc  38083  bndss  38124  isdrngo2  38296  divrngidl  38366  maxidlmax  38381  cdleme0nex  40753  dihglblem2N  41757  hgmapvs  42354  ismrcd1  43147  nacsfg  43154  isnacs3  43159  nacsfix  43161  mzpcl1  43178  mzpcl2  43179  mzpcong  43421  dnnumch1  43493  aomclem1  43503  aomclem6  43508  lnr2i  43565  hbtlem5  43577  hbt  43579  rexanuz3  45547  choicefi  45650  fsneq  45656  suplesup  45790  xralrple2  45805  infxr  45817  infleinf  45822  xralrple4  45823  xralrple3  45824  xrralrecnnge  45840  supxrunb3  45849  supxrleubrnmpt  45855  unb2ltle  45864  suprleubrnmpt  45871  infxrgelbrnmpt  45903  supminfxr  45913  xrpnf  45934  islpcn  46088  limclner  46100  climd  46121  clim2d  46122  limsupmnflem  46169  limsupre3uzlem  46184  xlimpnfxnegmnf  46263  xlimxrre  46280  xlimmnfvlem1  46281  xlimmnfv  46283  xlimpnfvlem1  46285  xlimpnfv  46287  climxlim2lem  46294  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  fourierdlem103  46658  fourierdlem104  46659  etransclem48  46731  saluncl  46766  subsaliuncllem  46806  sge0pnffigt  46845  omessle  46947  caragensplit  46949  omeunile  46954  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvle  47049  vonvolmbllem  47109  vonvolmbl  47110  pimdecfgtioc  47164  smfpreimalt  47180  smfpreimaltf  47185  smfpreimale  47203  smfpreimagt  47211  smfpreimage  47231  smfmullem4  47243  smfinflem  47266  iccpartrn  47905  iccpartiun  47909  icceuelpart  47911  lidldomn1  48722  ply1mulgsumlem2  48878  lindslinindsimp2lem5  48953  lindslinindsimp2  48954  snlindsntor  48962  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdig  49114