Theorem rspcva 3527

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2048  ∀wral 3082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-v 3411

This theorem is referenced by:  rexraleqim  3549  fvn0ssdmfun  6661  fveqdmss  6665  fvcofneq  6678  wfr3g  7749  boxriin  8293  boxcutc  8294  marypha1lem  8684  supmo  8703  infmo  8746  unwdomg  8835  isinffi  9207  axdc3lem2  9663  grothac  10042  nqereu  10141  nnsub  11477  zextle  11861  xrsupsslem  12509  xrinfmsslem  12510  supxrunb1  12521  supxrunb2  12522  injresinjlem  12965  ssnn0fi  13161  suppssfz  13170  faclbnd4lem4  13464  ishashinf  13624  rexuz3  14559  cau3lem  14565  caubnd2  14568  o1co  14794  climcn1  14799  incexclem  15041  dvdsext  15521  mreintcl  16714  initoeu1  17119  initoeu2  17124  termoeu1  17126  lublecllem  17446  mgmidmo  17717  gsumval2  17738  dfgrp3lem  17974  symgfix2  18295  odeq  18430  gexid  18457  gsummoncoe1  20165  m2detleiblem3  20932  m2detleiblem4  20933  cpmatmcllem  21020  mp2pm2mplem4  21111  cayleyhamilton1  21194  cmpsublem  21701  cmpsub  21702  cmpfii  21711  ptpjcn  21913  isufil2  22210  ufileu  22221  lmmbr  23554  caussi  23593  plyco0  24475  dgrco  24558  emcllem7  25271  isppw2  25384  uvtxnbgrvtx  26868  rusgrnumwwlks  27470  rusgrnumwwlksOLD  27471  clwwlkfOLD  27554  clwwlkf  27559  vdgn1frgrv2  27820  frgrregorufr  27849  grpoidinvlem3  28050  grpoideu  28053  lnconi  29581  fsumiunle  30280  rngurd  30492  tpr2rico  30756  esumiun  30954  0elsiga  30975  sigaclci  30993  dya2icoseg2  31138  signstfvneq0  31450  derangsn  31962  frr3g  32582  fwddifnp1  33087  poimirlem25  34306  poimirlem26  34307  poimirlem30  34311  poimirlem31  34312  poimirlem32  34313  heicant  34316  mblfinlem2  34319  ftc1anc  34364  fdc  34410  bndss  34454  isdrngo2  34626  divrngidl  34696  maxidlmax  34711  cdleme0nex  36819  dihglblem2N  37823  hgmapvs  38420  ismrcd1  38635  nacsfg  38642  isnacs3  38647  nacsfix  38649  mzpcl1  38666  mzpcl2  38667  mzpcong  38910  dnnumch1  38985  aomclem1  38995  aomclem4  38998  aomclem6  39000  lnr2i  39057  hbtlem5  39069  hbt  39071  pwssfi  40670  rexanuz3  40730  choicefi  40834  fsneq  40840  suplesup  40982  xralrple2  40997  infxr  41010  infleinf  41015  xralrple4  41016  xralrple3  41017  xrralrecnnge  41038  supxrunb3  41048  supxrleubrnmpt  41056  unb2ltle  41066  suprleubrnmpt  41073  infxrgelbrnmpt  41107  supminfxr  41117  xrpnf  41139  islpcn  41297  limclner  41309  climd  41330  clim2d  41331  limsupmnflem  41378  limsupre3uzlem  41393  liminflelimsuplem  41433  xlimpnfxnegmnf  41472  xlimxrre  41489  xlimmnfvlem1  41490  xlimmnfv  41492  xlimpnfvlem1  41494  xlimpnfv  41496  climxlim2lem  41503  ioodvbdlimc1lem1  41592  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  fourierdlem103  41871  fourierdlem104  41872  etransclem48  41944  saluncl  41979  subsaliuncllem  42017  sge0pnffigt  42055  omessle  42157  caragensplit  42159  omeunile  42164  hoidmvlelem2  42255  hoidmvlelem3  42256  hoidmvle  42259  vonvolmbllem  42319  vonvolmbl  42320  pimdecfgtioc  42370  smfpreimalt  42385  smfpreimaltf  42390  smfpreimale  42408  smfpreimagt  42415  smfpreimage  42435  smfmullem4  42446  smfinflem  42468  iccpartrn  42908  iccpartiun  42912  icceuelpart  42914  lidldomn1  43496  ply1mulgsumlem2  43748  lindslinindsimp2lem5  43824  lindslinindsimp2  43825  snlindsntor  43833  nn0sumshdiglemA  43987  nn0sumshdiglemB  43988  nn0sumshdig  43991