Theorem rspccv 3569

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 3568	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	com12 32	1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048

This theorem is referenced by:  elinti  4901  trss  5203  fvn0ssdmfun  7002  dff3  7028  2fvcoidd  7226  ofrval  7617  limsuc  7774  limuni3  7777  peano5  7818  frxp  8051  smo11  8279  odi  8489  supub  9338  suplub  9339  elirrvOLD  9479  dfom3  9532  noinfep  9545  tcrank  9772  alephle  9974  dfac5lem5  10013  dfac2b  10017  cofsmo  10155  coftr  10159  infpssrlem4  10192  isf34lem6  10266  axcc2lem  10322  domtriomlem  10328  axdc2lem  10334  axdc3lem2  10337  axdc4lem  10341  ac5b  10364  zorn2lem2  10383  zorn2lem6  10387  pwcfsdom  10469  inar1  10661  grupw  10681  grupr  10683  gruurn  10684  grothpw  10712  grothpwex  10713  axgroth6  10714  grothomex  10715  nqereu  10815  supsrlem  10997  axpre-sup  11055  dedekind  11271  dedekindle  11272  supmullem1  12087  supmul  12089  peano5nni  12123  dfnn2  12133  peano5uzi  12557  zindd  12569  lcmfdvds  16548  lcmfunsn  16550  1arith  16834  ramcl  16936  clatleglb  18419  pslem  18473  cyccom  19110  rngisomring1  20381  psgndiflemA  21533  eqcoe1ply1eq  22209  mvmumamul1  22464  smadiadetlem0  22571  chpscmat  22752  basis2  22861  tg2  22875  clsndisj  22985  cnpimaex  23166  t1sncld  23236  regsep  23244  nrmsep3  23265  cmpsub  23310  2ndc1stc  23361  refssex  23421  ptfinfin  23429  txcnpi  23518  txcmplem1  23551  tx1stc  23560  filss  23763  ufilss  23815  fclsopni  23925  fclsrest  23934  alexsubb  23956  alexsubALTlem2  23958  alexsubALTlem4  23960  ghmcnp  24025  qustgplem  24031  mopni  24402  metrest  24434  metcnpi  24454  metcnpi2  24455  nmolb  24627  nmoleub2lem2  25038  ovoliunlem1  25425  ovolicc2lem3  25442  mblsplit  25455  fta1b  26099  plycj  26205  plycjOLD  26207  lgamgulmlem1  26961  sqfpc  27069  ostth2lem2  27567  ostth3  27571  sltval2  27590  nogt01o  27630  madebdayim  27828  madebdaylemlrcut  27839  precsexlem9  28148  onsiso  28200  bdayon  28204  dfn0s2  28255  onsfi  28278  peano5uzs  28323  vdiscusgr  29505  0vtxrusgr  29551  rusgrnumwrdl2  29560  ewlkinedg  29578  eupthseg  30178  upgreupthseg  30181  numclwwlk1  30333  l2p  30451  lpni  30452  nvz  30641  chcompl  31214  ocin  31268  hmopidmchi  32123  dmdmd  32272  dmdbr5  32280  mdsl1i  32293  sigaclci  34137  bnj23  34722  kur14lem9  35250  sconnpht  35265  cvmsdisj  35306  sat1el2xp  35415  untelirr  35744  untsucf  35746  dfon2lem4  35820  dfon2lem6  35822  dfon2lem7  35823  dfon2lem8  35824  dfon2  35826  fwddifnp1  36199  domalom  37438  pibt2  37451  poimirlem18  37678  poimirlem21  37681  heibor1lem  37849  heiborlem4  37854  heiborlem6  37856  atlex  39355  psubspi  39786  elpcliN  39932  ldilval  40152  trlord  40608  tendotp  40800  hdmapval2  41871  cantnfresb  43357  pwelg  43593  gneispace0nelrn2  44174  gneispaceel2  44177  gneispacess2  44179  stoweid  46101  iccpartimp  47448  iccpartltu  47456  iccpartgtl  47457  iccpartleu  47459  iccpartgel  47460  isuspgrim0  47925  gricushgr  47948  1arymaptf1  48674