Theorem rspcva 3574

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rexraleqim  3601  fsneq  7028  fvn0ssdmfun  7068  fveqdmss  7072  fvcofneq  7087  wfr3g  8319  boxriin  8948  boxcutc  8949  pwssfi  9172  marypha1lem  9404  supmo  9423  infmo  9468  unwdomg  9557  frr3g  9739  isinffi  9998  axdc3lem2  10454  grothac  10840  nqereu  10939  nnsub  12305  zextle  12695  xrsupsslem  13360  xrinfmsslem  13361  supxrunb1  13372  supxrunb2  13373  injresinjlem  13847  ssnn0fi  14050  suppssfz  14059  faclbnd4lem4  14361  ishashinf  14529  rexuz3  15437  cau3lem  15443  caubnd2  15446  o1co  15674  climcn1  15680  incexclem  15926  dvdsext  16412  mreintcl  17680  initoeu1  18101  initoeu2  18106  termoeu1  18108  lublecllem  18447  mgmidmo  18753  gsumval2  18789  dfgrp3lem  19162  symgfix2  19544  odeq  19678  gexid  19709  ringurd  20325  o2timesd  20350  rglcom4d  20351  gsummoncoe1  22534  m2detleiblem3  22852  m2detleiblem4  22853  cpmatmcllem  22944  mp2pm2mplem4  23035  cayleyhamilton1  23118  cmpsublem  23625  cmpsub  23626  cmpfii  23635  ptpjcn  23838  isufil2  24135  ufileu  24146  lmmbr  25487  caussi  25526  plyco0  26418  dgrco  26502  emcllem7  27239  isppw2  27352  addsrid  28230  mulsrid  28379  n0subs  28629  uvtxnbgrvtx  29854  rusgrnumwwlks  30446  clwwlkf  30518  vdgn1frgrv2  30777  frgrregorufr  30806  grpoidinvlem3  30988  grpoideu  30991  lnconi  32515  fsumiunle  33300  tpr2rico  34423  esumiun  34605  0elsiga  34625  sigaclci  34643  dya2icoseg2  34790  derangsn  35750  sat1el2xp  35959  fwddifnp1  36746  poimirlem25  38395  poimirlem26  38396  poimirlem30  38400  poimirlem31  38401  poimirlem32  38402  heicant  38405  mblfinlem2  38408  ftc1anc  38451  fdc  38496  bndss  38537  isdrngo2  38709  divrngidl  38779  maxidlmax  38794  cdleme0nex  41164  dihglblem2N  42168  hgmapvs  42765  ismrcd1  43544  nacsfg  43551  isnacs3  43556  nacsfix  43558  mzpcl1  43575  mzpcl2  43576  mzpcong  43814  dnnumch1  43886  aomclem1  43896  aomclem6  43901  lnr2i  43958  hbtlem5  43970  hbt  43972  rexanuz3  45929  choicefi  46032  suplesup  46170  xralrple2  46185  infxr  46197  infleinf  46202  xralrple4  46203  xralrple3  46204  xrralrecnnge  46220  supxrunb3  46229  supxrleubrnmpt  46235  unb2ltle  46244  suprleubrnmpt  46251  infxrgelbrnmpt  46283  supminfxr  46293  xrpnf  46314  islpcn  46468  limclner  46480  climd  46501  clim2d  46502  limsupmnflem  46549  limsupre3uzlem  46564  xlimpnfxnegmnf  46643  xlimxrre  46660  xlimmnfvlem1  46661  xlimmnfv  46663  xlimpnfvlem1  46665  xlimpnfv  46667  climxlim2lem  46674  ioodvbdlimc1lem1  46760  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  fourierdlem103  47038  fourierdlem104  47039  etransclem48  47111  saluncl  47146  subsaliuncllem  47186  sge0pnffigt  47225  omessle  47327  caragensplit  47329  omeunile  47334  hoidmvlelem2  47425  hoidmvlelem3  47426  hoidmvle  47429  vonvolmbllem  47489  vonvolmbl  47490  pimdecfgtioc  47544  smfpreimalt  47560  smfpreimaltf  47565  smfpreimale  47583  smfpreimagt  47591  smfpreimage  47611  smfmullem4  47623  smfinflem  47646  iccpartrn  48331  iccpartiun  48335  icceuelpart  48337  lidldomn1  49147  ply1mulgsumlem2  49318  lindslinindsimp2lem5  49393  lindslinindsimp2  49394  snlindsntor  49402  nn0sumshdiglemA  49550  nn0sumshdiglemB  49551  nn0sumshdig  49554