Theorem rspccv 3604

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  ∀wral 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057

This theorem is referenced by:  elinti  4953  trss  5270  fvn0ssdmfun  7078  dff3  7104  2fvcoidd  7300  ofrval  7691  limsuc  7847  limuni3  7850  peano5  7893  frxp  8125  wfrdmclOLD  8331  smo11  8378  odi  8593  supub  9474  suplub  9475  elirrv  9611  dfom3  9662  noinfep  9675  tcrank  9899  alephle  10103  dfac5lem5  10142  dfac2b  10145  cofsmo  10284  coftr  10288  infpssrlem4  10321  isf34lem6  10395  axcc2lem  10451  domtriomlem  10457  axdc2lem  10463  axdc3lem2  10466  axdc4lem  10470  ac5b  10493  zorn2lem2  10512  zorn2lem6  10516  pwcfsdom  10598  inar1  10790  grupw  10810  grupr  10812  gruurn  10813  grothpw  10841  grothpwex  10842  axgroth6  10843  grothomex  10844  nqereu  10944  supsrlem  11126  axpre-sup  11184  dedekind  11399  dedekindle  11400  supmullem1  12206  supmul  12208  peano5nni  12237  dfnn2  12247  peano5uzi  12673  zindd  12685  lcmfdvds  16604  lcmfunsn  16606  1arith  16887  ramcl  16989  clatleglb  18501  pslem  18555  cyccom  19149  rngisomring1  20396  psgndiflemA  21520  eqcoe1ply1eq  22205  mvmumamul1  22443  smadiadetlem0  22550  chpscmat  22731  basis2  22841  tg2  22855  clsndisj  22966  cnpimaex  23147  t1sncld  23217  regsep  23225  nrmsep3  23246  cmpsub  23291  2ndc1stc  23342  refssex  23402  ptfinfin  23410  txcnpi  23499  txcmplem1  23532  tx1stc  23541  filss  23744  ufilss  23796  fclsopni  23906  fclsrest  23915  alexsubb  23937  alexsubALTlem2  23939  alexsubALTlem4  23941  ghmcnp  24006  qustgplem  24012  mopni  24388  metrest  24420  metcnpi  24440  metcnpi2  24441  nmolb  24621  nmoleub2lem2  25030  ovoliunlem1  25418  ovolicc2lem3  25435  mblsplit  25448  fta1b  26093  plycj  26199  lgamgulmlem1  26948  sqfpc  27056  ostth2lem2  27554  ostth3  27558  sltval2  27576  nogt01o  27616  madebdayim  27801  madebdaylemlrcut  27812  precsexlem9  28100  dfn0s2  28188  vdiscusgr  29332  0vtxrusgr  29378  rusgrnumwrdl2  29387  ewlkinedg  29405  eupthseg  30003  upgreupthseg  30006  numclwwlk1  30158  l2p  30276  lpni  30277  nvz  30466  chcompl  31039  ocin  31093  hmopidmchi  31948  dmdmd  32097  dmdbr5  32105  mdsl1i  32118  sigaclci  33687  bnj23  34285  kur14lem9  34760  sconnpht  34775  cvmsdisj  34816  sat1el2xp  34925  untelirr  35238  untsucf  35240  dfon2lem4  35318  dfon2lem6  35320  dfon2lem7  35321  dfon2lem8  35322  dfon2  35324  fwddifnp1  35697  domalom  36819  pibt2  36832  poimirlem18  37046  poimirlem21  37049  heibor1lem  37217  heiborlem4  37222  heiborlem6  37224  atlex  38725  psubspi  39157  elpcliN  39303  ldilval  39523  trlord  39979  tendotp  40171  hdmapval2  41242  cantnfresb  42676  pwelg  42913  gneispace0nelrn2  43494  gneispaceel2  43497  gneispacess2  43499  stoweid  45374  iccpartimp  46680  iccpartltu  46688  iccpartgtl  46689  iccpartleu  46691  iccpartgel  46692  isuspgrim0  47093  gricushgr  47106  1arymaptf1  47638