Theorem rspcva 3280

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175

This theorem is referenced by:  rexraleqim  3299  n0snor2el  4304  fvn0ssdmfun  6258  fveqdmss  6262  fvcofneq  6275  caofinvl  6822  tfisi  6950  suppssov1  7214  wfr3g  7300  wfrlem17  7318  tfrlem1  7359  boxriin  7836  boxcutc  7837  marypha1lem  8222  marypha1  8223  supmo  8241  infmo  8284  wemaplem2  8335  unwdomg  8372  isinffi  8701  dfac9  8841  sornom  8982  fin23lem11  9022  fin1a2lem13  9117  axdc3lem2  9156  winalim2  9397  grothac  9531  nqereu  9630  nnsub  10936  zextle  11326  xrsupsslem  12009  xrinfmsslem  12010  supxrunb1  12021  supxrunb2  12022  injresinjlem  12450  ssnn0fi  12646  suppssfz  12656  faclbnd4lem4  12945  ishashinf  13104  rexuz3  13936  cau3lem  13942  caubnd2  13945  o1co  14165  climcn1  14170  incexclem  14407  dvdsext  14881  cshwsidrepsw  15638  prdsbasprj  15955  mreintcl  16078  isacs2  16137  acsfiel  16138  initoeu1  16484  initoeu2  16489  termoeu1  16491  isdrs2  16762  lublecllem  16811  joinle  16837  meetle  16851  acsdrsel  16990  isacs4lem  16991  isacs5lem  16992  acsdrscl  16993  acsficl  16994  mgmidmo  17082  gsumval2  17103  mrcmndind  17189  dfgrp3lem  17336  symgfix2  17659  odeq  17792  gexid  17819  mplind  19323  gsummoncoe1  19495  psgndiflemB  19765  mdetunilem1  20237  m2detleiblem3  20254  m2detleiblem4  20255  cpmatmcllem  20342  mp2pm2mplem4  20433  cayleyhamilton1  20516  cmpsublem  21012  cmpsub  21013  hauscmplem  21019  cmpfii  21022  ptpjcn  21224  isufil2  21522  ufileu  21533  isucn2  21893  cfiluweak  21909  cuspcvg  21915  lpbl  22118  lmmbr  22864  caussi  22903  mdeglt  23629  deg1lt  23661  ply1divex  23700  plyco0  23752  dgrco  23835  emcllem7  24528  isppw2  24641  pntleme  25097  pntlemp  25099  tglowdim2ln  25346  nbcusgra  25992  uvtxnbgra  26021  wlkdvspthlem  26137  clwwlkf  26322  rusgranumwlks  26483  frgraunss  26522  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  frgrancvvdeqlem4  26560  frgraregorufr  26580  extwwlkfablem1  26601  grpoidinvlem3  26744  grpoideu  26747  lnconi  28276  rngurd  29119  tpr2rico  29286  esumiun  29483  ofcfeqd2  29490  0elsiga  29504  sigaclci  29522  dya2icoseg2  29667  signstfvneq0  29975  derangsn  30406  frr3g  31023  fwddifnp1  31442  poimirlem25  32604  poimirlem26  32605  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  heicant  32614  mblfinlem2  32617  ftc1anc  32663  fdc  32711  bndss  32755  isdrngo2  32927  divrngidl  32997  maxidlmax  33012  cdleme0nex  34595  dihglblem2N  35601  hgmapvs  36201  ismrcd1  36279  nacsfg  36286  isnacs3  36291  nacsfix  36293  mzpcl1  36310  mzpcl2  36311  mzpcong  36557  dnnumch1  36632  fnwe2lem2  36639  aomclem1  36642  aomclem4  36645  aomclem6  36647  lnr2i  36705  hbtlem5  36717  hbt  36719  pwssfi  38236  eliind  38266  rexanuz3  38303  choicefi  38387  fsneq  38393  suplesup  38496  xralrple2  38511  infxr  38524  infleinf  38529  xralrple4  38530  xralrple3  38531  xrralrecnnge  38554  islpcn  38706  limclner  38718  climd  38739  clim2d  38740  cncfshift  38759  cncfperiod  38764  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  fourierdlem103  39102  fourierdlem104  39103  etransclem48  39175  salunicl  39212  saluncl  39213  saldifcl  39215  subsaliuncllem  39251  sge0pnffigt  39289  meadjuni  39350  omessle  39388  caragensplit  39390  omeunile  39395  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvle  39490  vonvolmbllem  39550  vonvolmbl  39551  pimdecfgtioc  39602  smfpreimalt  39617  smfpreimaltf  39623  smfpreimale  39641  smfpreimagt  39648  smfpreimage  39668  smfmullem4  39679  iccpartimp  39955  iccpartrn  39968  iccpartiun  39972  icceuelpart  39974  reuccatpfxs1  40297  uvtxanbgrvtx  40619  rusgrnumwwlks  41177  clwwlksf  41222  eupthseg  41374  upgreupthseg  41377  vdgn1frgrv2  41466  frgrncvvdeqlem4  41472  frgrregorufr  41490  av-extwwlkfablem1  41508  lidldomn1  41711  ply1mulgsumlem2  41969  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  snlindsntor  42054  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdig  42215