Theorem rspccv 3632

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspccv	⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspccv

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3631	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	com12 32	1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  elinti  4979  trss  5294  fvn0ssdmfun  7108  dff3  7134  2fvcoidd  7333  ofrval  7726  limsuc  7886  limuni3  7889  peano5  7932  frxp  8167  wfrdmclOLD  8373  smo11  8420  odi  8635  supub  9528  suplub  9529  elirrv  9665  dfom3  9716  noinfep  9729  tcrank  9953  alephle  10157  dfac5lem5  10196  dfac2b  10200  cofsmo  10338  coftr  10342  infpssrlem4  10375  isf34lem6  10449  axcc2lem  10505  domtriomlem  10511  axdc2lem  10517  axdc3lem2  10520  axdc4lem  10524  ac5b  10547  zorn2lem2  10566  zorn2lem6  10570  pwcfsdom  10652  inar1  10844  grupw  10864  grupr  10866  gruurn  10867  grothpw  10895  grothpwex  10896  axgroth6  10897  grothomex  10898  nqereu  10998  supsrlem  11180  axpre-sup  11238  dedekind  11453  dedekindle  11454  supmullem1  12265  supmul  12267  peano5nni  12296  dfnn2  12306  peano5uzi  12732  zindd  12744  lcmfdvds  16689  lcmfunsn  16691  1arith  16974  ramcl  17076  clatleglb  18588  pslem  18642  cyccom  19243  rngisomring1  20494  psgndiflemA  21642  eqcoe1ply1eq  22324  mvmumamul1  22581  smadiadetlem0  22688  chpscmat  22869  basis2  22979  tg2  22993  clsndisj  23104  cnpimaex  23285  t1sncld  23355  regsep  23363  nrmsep3  23384  cmpsub  23429  2ndc1stc  23480  refssex  23540  ptfinfin  23548  txcnpi  23637  txcmplem1  23670  tx1stc  23679  filss  23882  ufilss  23934  fclsopni  24044  fclsrest  24053  alexsubb  24075  alexsubALTlem2  24077  alexsubALTlem4  24079  ghmcnp  24144  qustgplem  24150  mopni  24526  metrest  24558  metcnpi  24578  metcnpi2  24579  nmolb  24759  nmoleub2lem2  25168  ovoliunlem1  25556  ovolicc2lem3  25573  mblsplit  25586  fta1b  26231  plycj  26337  lgamgulmlem1  27090  sqfpc  27198  ostth2lem2  27696  ostth3  27700  sltval2  27719  nogt01o  27759  madebdayim  27944  madebdaylemlrcut  27955  precsexlem9  28257  dfn0s2  28354  peano5uzs  28408  vdiscusgr  29567  0vtxrusgr  29613  rusgrnumwrdl2  29622  ewlkinedg  29640  eupthseg  30238  upgreupthseg  30241  numclwwlk1  30393  l2p  30511  lpni  30512  nvz  30701  chcompl  31274  ocin  31328  hmopidmchi  32183  dmdmd  32332  dmdbr5  32340  mdsl1i  32353  sigaclci  34096  bnj23  34694  kur14lem9  35182  sconnpht  35197  cvmsdisj  35238  sat1el2xp  35347  untelirr  35670  untsucf  35672  dfon2lem4  35750  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  fwddifnp1  36129  domalom  37370  pibt2  37383  poimirlem18  37598  poimirlem21  37601  heibor1lem  37769  heiborlem4  37774  heiborlem6  37776  atlex  39272  psubspi  39704  elpcliN  39850  ldilval  40070  trlord  40526  tendotp  40718  hdmapval2  41789  cantnfresb  43286  pwelg  43522  gneispace0nelrn2  44103  gneispaceel2  44106  gneispacess2  44108  stoweid  45984  iccpartimp  47291  iccpartltu  47299  iccpartgtl  47300  iccpartleu  47302  iccpartgel  47303  isuspgrim0  47756  gricushgr  47770  1arymaptf1  48376