Theorem rspccv 3618

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059

This theorem is referenced by:  elinti  4959  trss  5275  fvn0ssdmfun  7093  dff3  7119  2fvcoidd  7316  ofrval  7708  limsuc  7869  limuni3  7872  peano5  7915  frxp  8149  wfrdmclOLD  8355  smo11  8402  odi  8615  supub  9496  suplub  9497  elirrv  9633  dfom3  9684  noinfep  9697  tcrank  9921  alephle  10125  dfac5lem5  10164  dfac2b  10168  cofsmo  10306  coftr  10310  infpssrlem4  10343  isf34lem6  10417  axcc2lem  10473  domtriomlem  10479  axdc2lem  10485  axdc3lem2  10488  axdc4lem  10492  ac5b  10515  zorn2lem2  10534  zorn2lem6  10538  pwcfsdom  10620  inar1  10812  grupw  10832  grupr  10834  gruurn  10835  grothpw  10863  grothpwex  10864  axgroth6  10865  grothomex  10866  nqereu  10966  supsrlem  11148  axpre-sup  11206  dedekind  11421  dedekindle  11422  supmullem1  12235  supmul  12237  peano5nni  12266  dfnn2  12276  peano5uzi  12704  zindd  12716  lcmfdvds  16675  lcmfunsn  16677  1arith  16960  ramcl  17062  clatleglb  18575  pslem  18629  cyccom  19233  rngisomring1  20484  psgndiflemA  21636  eqcoe1ply1eq  22318  mvmumamul1  22575  smadiadetlem0  22682  chpscmat  22863  basis2  22973  tg2  22987  clsndisj  23098  cnpimaex  23279  t1sncld  23349  regsep  23357  nrmsep3  23378  cmpsub  23423  2ndc1stc  23474  refssex  23534  ptfinfin  23542  txcnpi  23631  txcmplem1  23664  tx1stc  23673  filss  23876  ufilss  23928  fclsopni  24038  fclsrest  24047  alexsubb  24069  alexsubALTlem2  24071  alexsubALTlem4  24073  ghmcnp  24138  qustgplem  24144  mopni  24520  metrest  24552  metcnpi  24572  metcnpi2  24573  nmolb  24753  nmoleub2lem2  25162  ovoliunlem1  25550  ovolicc2lem3  25567  mblsplit  25580  fta1b  26225  plycj  26331  plycjOLD  26333  lgamgulmlem1  27086  sqfpc  27194  ostth2lem2  27692  ostth3  27696  sltval2  27715  nogt01o  27755  madebdayim  27940  madebdaylemlrcut  27951  precsexlem9  28253  dfn0s2  28350  peano5uzs  28404  vdiscusgr  29563  0vtxrusgr  29609  rusgrnumwrdl2  29618  ewlkinedg  29636  eupthseg  30234  upgreupthseg  30237  numclwwlk1  30389  l2p  30507  lpni  30508  nvz  30697  chcompl  31270  ocin  31324  hmopidmchi  32179  dmdmd  32328  dmdbr5  32336  mdsl1i  32349  sigaclci  34112  bnj23  34710  kur14lem9  35198  sconnpht  35213  cvmsdisj  35254  sat1el2xp  35363  untelirr  35687  untsucf  35689  dfon2lem4  35767  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  dfon2  35773  fwddifnp1  36146  domalom  37386  pibt2  37399  poimirlem18  37624  poimirlem21  37627  heibor1lem  37795  heiborlem4  37800  heiborlem6  37802  atlex  39297  psubspi  39729  elpcliN  39875  ldilval  40095  trlord  40551  tendotp  40743  hdmapval2  41814  cantnfresb  43313  pwelg  43549  gneispace0nelrn2  44130  gneispaceel2  44133  gneispacess2  44135  stoweid  46018  iccpartimp  47341  iccpartltu  47349  iccpartgtl  47350  iccpartleu  47352  iccpartgel  47353  isuspgrim0  47809  gricushgr  47823  1arymaptf1  48491