Theorem rspcva 3570

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048

This theorem is referenced by:  rexraleqim  3597  fvn0ssdmfun  7007  fveqdmss  7011  fvcofneq  7026  wfr3g  8249  boxriin  8864  boxcutc  8865  pwssfi  9086  marypha1lem  9317  supmo  9336  infmo  9381  unwdomg  9470  frr3g  9649  isinffi  9885  axdc3lem2  10342  grothac  10721  nqereu  10820  nnsub  12169  zextle  12546  xrsupsslem  13206  xrinfmsslem  13207  supxrunb1  13218  supxrunb2  13219  injresinjlem  13690  ssnn0fi  13892  suppssfz  13901  faclbnd4lem4  14203  ishashinf  14370  rexuz3  15256  cau3lem  15262  caubnd2  15265  o1co  15493  climcn1  15499  incexclem  15743  dvdsext  16232  mreintcl  17497  initoeu1  17918  initoeu2  17923  termoeu1  17925  lublecllem  18264  mgmidmo  18568  gsumval2  18594  dfgrp3lem  18951  symgfix2  19328  odeq  19462  gexid  19493  ringurd  20103  o2timesd  20128  rglcom4d  20129  gsummoncoe1  22223  m2detleiblem3  22544  m2detleiblem4  22545  cpmatmcllem  22633  mp2pm2mplem4  22724  cayleyhamilton1  22807  cmpsublem  23314  cmpsub  23315  cmpfii  23324  ptpjcn  23526  isufil2  23823  ufileu  23834  lmmbr  25185  caussi  25224  plyco0  26124  dgrco  26208  emcllem7  26939  isppw2  27052  addsrid  27907  mulsrid  28052  n0subs  28289  uvtxnbgrvtx  29371  rusgrnumwwlks  29955  clwwlkf  30027  vdgn1frgrv2  30276  frgrregorufr  30305  grpoidinvlem3  30486  grpoideu  30489  lnconi  32013  fsumiunle  32812  tpr2rico  33925  esumiun  34107  0elsiga  34127  sigaclci  34145  dya2icoseg2  34291  derangsn  35214  sat1el2xp  35423  fwddifnp1  36209  poimirlem25  37695  poimirlem26  37696  poimirlem30  37700  poimirlem31  37701  poimirlem32  37702  heicant  37705  mblfinlem2  37708  ftc1anc  37751  fdc  37795  bndss  37836  isdrngo2  38008  divrngidl  38078  maxidlmax  38093  cdleme0nex  40399  dihglblem2N  41403  hgmapvs  42000  ismrcd1  42801  nacsfg  42808  isnacs3  42813  nacsfix  42815  mzpcl1  42832  mzpcl2  42833  mzpcong  43075  dnnumch1  43147  aomclem1  43157  aomclem6  43162  lnr2i  43219  hbtlem5  43231  hbt  43233  rexanuz3  45203  choicefi  45307  fsneq  45313  suplesup  45448  xralrple2  45463  infxr  45475  infleinf  45480  xralrple4  45481  xralrple3  45482  xrralrecnnge  45498  supxrunb3  45507  supxrleubrnmpt  45514  unb2ltle  45523  suprleubrnmpt  45530  infxrgelbrnmpt  45562  supminfxr  45572  xrpnf  45593  islpcn  45747  limclner  45759  climd  45780  clim2d  45781  limsupmnflem  45828  limsupre3uzlem  45843  xlimpnfxnegmnf  45922  xlimxrre  45939  xlimmnfvlem1  45940  xlimmnfv  45942  xlimpnfvlem1  45944  xlimpnfv  45946  climxlim2lem  45953  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  fourierdlem103  46317  fourierdlem104  46318  etransclem48  46390  saluncl  46425  subsaliuncllem  46465  sge0pnffigt  46504  omessle  46606  caragensplit  46608  omeunile  46613  hoidmvlelem2  46704  hoidmvlelem3  46705  hoidmvle  46708  vonvolmbllem  46768  vonvolmbl  46769  pimdecfgtioc  46823  smfpreimalt  46839  smfpreimaltf  46844  smfpreimale  46862  smfpreimagt  46870  smfpreimage  46890  smfmullem4  46902  smfinflem  46925  iccpartrn  47540  iccpartiun  47544  icceuelpart  47546  lidldomn1  48341  ply1mulgsumlem2  48498  lindslinindsimp2lem5  48573  lindslinindsimp2  48574  snlindsntor  48582  nn0sumshdiglemA  48730  nn0sumshdiglemB  48731  nn0sumshdig  48734