Theorem rspcva 3575

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is used by:  rexraleqim  3601  fsneq  7034  fvn0ssdmfun  7074  fveqdmss  7078  fvcofneq  7093  wfr3g  8337  boxriin  8968  boxcutc  8969  pwssfi  9192  marypha1lem  9425  supmo  9444  infmo  9489  unwdomg  9578  frr3g  9760  hfelhf  9914  isinffi  10073  axdc3lem2  10529  grothac  10915  nqereu  11014  nnsub  12382  zextle  12772  xrsupsslem  13437  xrinfmsslem  13438  supxrunb1  13449  supxrunb2  13450  injresinjlem  13925  ssnn0fi  14128  suppssfz  14137  faclbnd4lem4  14440  ishashinf  14608  rexuz3  15516  cau3lem  15522  caubnd2  15525  o1co  15753  climcn1  15759  incexclem  16005  dvdsext  16491  mreintcl  17765  initoeu1  18186  initoeu2  18191  termoeu1  18193  lublecllem  18532  mgmidmo  18838  gsumval2  18875  dfgrp3lem  19248  symgfix2  19630  odeq  19764  gexid  19795  ringurd  20411  o2timesd  20436  rglcom4d  20437  gsummoncoe1  22626  m2detleiblem3  22944  m2detleiblem4  22945  cpmatmcllem  23036  mp2pm2mplem4  23127  cayleyhamilton1  23210  cmpsublem  23717  cmpsub  23718  cmpfii  23727  ptpjcn  23930  isufil2  24227  ufileu  24238  lmmbr  25579  caussi  25618  plyco0  26510  dgrco  26594  emcllem7  27329  isppw2  27442  addsrid  28350  mulsrid  28499  n0subs  28749  uvtxnbgrvtx  29974  rusgrnumwwlks  30566  clwwlkf  30638  vdgn1frgrv2  30897  frgrregorufr  30926  grpoidinvlem3  31108  grpoideu  31111  lnconi  32635  fsumiunle  33420  tpr2rico  34544  esumiun  34726  0elsiga  34746  sigaclci  34764  dya2icoseg2  34910  derangsn  35935  sat1el2xp  36144  fwddifnp1  36930  poimirlem25  38563  poimirlem26  38564  poimirlem30  38568  poimirlem31  38569  poimirlem32  38570  heicant  38573  mblfinlem2  38576  ftc1anc  38619  fdc  38679  bndss  38720  isdrngo2  38892  divrngidl  38962  maxidlmax  38977  cdleme0nex  41347  dihglblem2N  42351  hgmapvs  42948  ismrcd1  43708  nacsfg  43715  isnacs3  43720  nacsfix  43722  mzpcl1  43739  mzpcl2  43740  mzpcong  43978  dnnumch1  44050  aomclem1  44055  aomclem6  44060  lnr2i  44117  hbtlem5  44129  hbt  44131  rexanuz3  46110  choicefi  46213  suplesup  46350  xralrple2  46365  infxr  46377  infleinf  46382  xralrple4  46383  xralrple3  46384  xrralrecnnge  46400  supxrunb3  46409  supxrleubrnmpt  46415  unb2ltle  46424  suprleubrnmpt  46431  infxrgelbrnmpt  46463  supminfxr  46473  xrpnf  46494  islpcn  46648  limclner  46660  climd  46681  clim2d  46682  limsupmnflem  46729  limsupre3uzlem  46744  xlimpnfxnegmnf  46823  xlimxrre  46840  xlimmnfvlem1  46841  xlimmnfv  46843  xlimpnfvlem1  46845  xlimpnfv  46847  climxlim2lem  46854  ioodvbdlimc1lem1  46940  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  fourierdlem103  47218  fourierdlem104  47219  etransclem48  47291  saluncl  47326  subsaliuncllem  47366  sge0pnffigt  47405  omessle  47507  caragensplit  47509  omeunile  47514  hoidmvlelem2  47605  hoidmvlelem3  47606  hoidmvle  47609  vonvolmbllem  47669  vonvolmbl  47670  pimdecfgtioc  47724  smfpreimalt  47740  smfpreimaltf  47745  smfpreimale  47763  smfpreimagt  47771  smfpreimage  47791  smfmullem4  47803  smfinflem  47826  iccpartrn  48511  iccpartiun  48515  icceuelpart  48517  lidldomn1  49327  ply1mulgsumlem2  49498  lindslinindsimp2lem5  49573  lindslinindsimp2  49574  snlindsntor  49582  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdig  49734