Theorem rspcva 3535

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066

This theorem is referenced by:  rexraleqim  3554  fvn0ssdmfun  6895  fveqdmss  6899  fvcofneq  6912  wfr3g  8053  boxriin  8621  boxcutc  8622  marypha1lem  9049  supmo  9068  infmo  9111  unwdomg  9200  frr3g  9372  isinffi  9608  axdc3lem2  10065  grothac  10444  nqereu  10543  nnsub  11874  zextle  12250  xrsupsslem  12897  xrinfmsslem  12898  supxrunb1  12909  supxrunb2  12910  injresinjlem  13362  ssnn0fi  13558  suppssfz  13567  faclbnd4lem4  13862  ishashinf  14029  rexuz3  14912  cau3lem  14918  caubnd2  14921  o1co  15147  climcn1  15153  incexclem  15400  dvdsext  15882  mreintcl  17098  initoeu1  17517  initoeu2  17522  termoeu1  17524  lublecllem  17866  mgmidmo  18132  gsumval2  18158  dfgrp3lem  18461  symgfix2  18808  odeq  18942  gexid  18970  gsummoncoe1  21225  m2detleiblem3  21526  m2detleiblem4  21527  cpmatmcllem  21615  mp2pm2mplem4  21706  cayleyhamilton1  21789  cmpsublem  22296  cmpsub  22297  cmpfii  22306  ptpjcn  22508  isufil2  22805  ufileu  22816  lmmbr  24155  caussi  24194  plyco0  25086  dgrco  25169  emcllem7  25884  isppw2  25997  uvtxnbgrvtx  27481  rusgrnumwwlks  28058  clwwlkf  28130  vdgn1frgrv2  28379  frgrregorufr  28408  grpoidinvlem3  28587  grpoideu  28590  lnconi  30114  fsumiunle  30863  rngurd  31201  tpr2rico  31576  esumiun  31774  0elsiga  31794  sigaclci  31812  dya2icoseg2  31957  derangsn  32845  sat1el2xp  33054  addsid1  33864  fwddifnp1  34204  poimirlem25  35539  poimirlem26  35540  poimirlem30  35544  poimirlem31  35545  poimirlem32  35546  heicant  35549  mblfinlem2  35552  ftc1anc  35595  fdc  35640  bndss  35681  isdrngo2  35853  divrngidl  35923  maxidlmax  35938  cdleme0nex  38041  dihglblem2N  39045  hgmapvs  39642  ismrcd1  40223  nacsfg  40230  isnacs3  40235  nacsfix  40237  mzpcl1  40254  mzpcl2  40255  mzpcong  40497  dnnumch1  40572  aomclem1  40582  aomclem6  40587  lnr2i  40644  hbtlem5  40656  hbt  40658  pwssfi  42266  rexanuz3  42319  choicefi  42413  fsneq  42419  suplesup  42551  xralrple2  42566  infxr  42579  infleinf  42584  xralrple4  42585  xralrple3  42586  xrralrecnnge  42603  supxrunb3  42612  supxrleubrnmpt  42619  unb2ltle  42628  suprleubrnmpt  42635  infxrgelbrnmpt  42669  supminfxr  42679  xrpnf  42701  islpcn  42855  limclner  42867  climd  42888  clim2d  42889  limsupmnflem  42936  limsupre3uzlem  42951  liminflelimsuplem  42991  xlimpnfxnegmnf  43030  xlimxrre  43047  xlimmnfvlem1  43048  xlimmnfv  43050  xlimpnfvlem1  43052  xlimpnfv  43054  climxlim2lem  43061  ioodvbdlimc1lem1  43147  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  fourierdlem103  43425  fourierdlem104  43426  etransclem48  43498  saluncl  43533  subsaliuncllem  43571  sge0pnffigt  43609  omessle  43711  caragensplit  43713  omeunile  43718  hoidmvlelem2  43809  hoidmvlelem3  43810  hoidmvle  43813  vonvolmbllem  43873  vonvolmbl  43874  pimdecfgtioc  43924  smfpreimalt  43939  smfpreimaltf  43944  smfpreimale  43962  smfpreimagt  43969  smfpreimage  43989  smfmullem4  44000  smfinflem  44022  iccpartrn  44555  iccpartiun  44559  icceuelpart  44561  lidldomn1  45152  ply1mulgsumlem2  45401  lindslinindsimp2lem5  45476  lindslinindsimp2  45477  snlindsntor  45485  nn0sumshdiglemA  45638  nn0sumshdiglemB  45639  nn0sumshdig  45642