Theorem rspccv 3587

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  elinti  4922  trss  5229  fvn0ssdmfun  7067  dff3  7093  2fvcoidd  7293  ofrval  7684  limsuc  7841  limuni3  7844  peano5  7886  frxp  8118  smo11  8347  odi  8560  supub  9415  suplub  9416  elirrvOLDOLD  9557  dfom3  9612  noinfep  9625  tcrank  9852  alephle  10068  dfac5lem5  10107  dfac2b  10110  cofsmo  10249  coftr  10253  infpssrlem4  10286  isf34lem6  10360  axcc2lem  10416  domtriomlem  10422  axdc2lem  10428  axdc3lem2  10431  axdc4lem  10435  ac5b  10458  zorn2lem2  10477  zorn2lem6  10481  pwcfsdom  10564  inar1  10756  grupw  10776  grupr  10778  gruurn  10779  grothpw  10807  grothpwex  10808  axgroth6  10809  grothomex  10810  nqereu  10910  supsrlem  11092  axpre-sup  11150  dedekind  11369  dedekindle  11370  supmullem1  12181  supmul  12183  peano5nni  12232  dfnn2  12242  peano5uzi  12681  zindd  12693  lcmfdvds  16696  lcmfunsn  16698  1arith  16983  ramcl  17085  clatleglb  18570  pslem  18624  cyccom  19270  rngisomring1  20546  psgndiflemA  21716  eqcoe1ply1eq  22424  mvmumamul1  22676  smadiadetlem0  22783  chpscmat  22964  basis2  23073  tg2  23087  clsndisj  23197  cnpimaex  23378  t1sncld  23448  regsep  23456  nrmsep3  23477  cmpsub  23522  2ndc1stc  23573  refssex  23633  ptfinfin  23641  txcnpi  23730  txcmplem1  23763  tx1stc  23772  filss  23975  ufilss  24027  fclsopni  24137  fclsrest  24146  alexsubb  24168  alexsubALTlem2  24170  alexsubALTlem4  24172  ghmcnp  24237  qustgplem  24243  mopni  24614  metrest  24646  metcnpi  24666  metcnpi2  24667  nmolb  24839  nmoleub2lem2  25240  ovoliunlem1  25626  ovolicc2lem3  25643  mblsplit  25656  fta1b  26294  plycj  26399  plycjOLD  26401  lgamgulmlem1  27155  sqfpc  27263  ostth2lem2  27760  ostth3  27764  ltsval2  27782  nogt01o  27822  madebdayim  28043  madebdaylemlrcut  28054  precsexlem9  28370  oniso  28426  bdayons  28431  dfn0s2  28487  onsfi  28511  peano5uzs  28559  bdaypw2n0bndlem  28618  vdiscusgr  29818  0vtxrusgr  29864  rusgrnumwrdl2  29873  ewlkinedg  29891  eupthseg  30494  upgreupthseg  30497  numclwwlk1  30649  l2p  30768  lpni  30769  nvz  30958  chcompl  31531  ocin  31585  hmopidmchi  32440  dmdmd  32589  dmdbr5  32597  mdsl1i  32610  sigaclci  34463  bnj23  35048  kur14lem9  35601  sconnpht  35616  cvmsdisj  35657  sat1el2xp  35766  untelirr  36095  untsucf  36097  dfon2lem4  36171  dfon2lem6  36173  dfon2lem7  36174  dfon2lem8  36175  dfon2  36177  fwddifnp1  36552  domalom  37933  pibt2  37946  poimirlem18  38172  poimirlem21  38175  heibor1lem  38343  heiborlem4  38348  heiborlem6  38350  atlex  39975  psubspi  40406  elpcliN  40552  ldilval  40772  trlord  41228  tendotp  41420  hdmapval2  42491  cantnfresb  43938  pwelg  44173  gneispace0nelrn2  44754  gneispaceel2  44757  gneispacess2  44759  stoweid  46664  iccpartimp  48050  iccpartltu  48058  iccpartgtl  48059  iccpartleu  48061  iccpartgel  48062  isuspgrim0  48543  gricushgr  48566  1arymaptf1  49302