Theorem rspccv 3549

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068

This theorem is referenced by:  elinti  4885  trss  5196  fvn0ssdmfun  6934  dff3  6958  2fvcoidd  7149  ofrval  7523  limsuc  7671  limuni3  7674  peano5  7714  frxp  7938  wfrdmclOLD  8119  smo11  8166  odi  8372  supub  9148  suplub  9149  elirrv  9285  dfom3  9335  noinfep  9348  tcrank  9573  alephle  9775  dfac5lem5  9814  dfac2b  9817  cofsmo  9956  coftr  9960  infpssrlem4  9993  isf34lem6  10067  axcc2lem  10123  domtriomlem  10129  axdc2lem  10135  axdc3lem2  10138  axdc4lem  10142  ac5b  10165  zorn2lem2  10184  zorn2lem6  10188  pwcfsdom  10270  inar1  10462  grupw  10482  grupr  10484  gruurn  10485  grothpw  10513  grothpwex  10514  axgroth6  10515  grothomex  10516  nqereu  10616  supsrlem  10798  axpre-sup  10856  dedekind  11068  dedekindle  11069  supmullem1  11875  supmul  11877  peano5nni  11906  dfnn2  11916  peano5uzi  12339  zindd  12351  lcmfdvds  16275  lcmfunsn  16277  1arith  16556  ramcl  16658  clatleglb  18151  pslem  18205  cyccom  18737  cygablOLD  19407  psgndiflemA  20718  eqcoe1ply1eq  21378  mvmumamul1  21611  smadiadetlem0  21718  chpscmat  21899  basis2  22009  tg2  22023  clsndisj  22134  cnpimaex  22315  t1sncld  22385  regsep  22393  nrmsep3  22414  cmpsub  22459  2ndc1stc  22510  refssex  22570  ptfinfin  22578  txcnpi  22667  txcmplem1  22700  tx1stc  22709  filss  22912  ufilss  22964  fclsopni  23074  fclsrest  23083  alexsubb  23105  alexsubALTlem2  23107  alexsubALTlem4  23109  ghmcnp  23174  qustgplem  23180  mopni  23554  metrest  23586  metcnpi  23606  metcnpi2  23607  nmolb  23787  nmoleub2lem2  24185  ovoliunlem1  24571  ovolicc2lem3  24588  mblsplit  24601  fta1b  25239  plycj  25343  lgamgulmlem1  26083  sqfpc  26191  ostth2lem2  26687  ostth3  26691  vdiscusgr  27801  0vtxrusgr  27847  rusgrnumwrdl2  27856  ewlkinedg  27874  eupthseg  28471  upgreupthseg  28474  numclwwlk1  28626  l2p  28742  lpni  28743  nvz  28932  chcompl  29505  ocin  29559  hmopidmchi  30414  dmdmd  30563  dmdbr5  30571  mdsl1i  30584  sigaclci  32000  bnj23  32597  kur14lem9  33076  sconnpht  33091  cvmsdisj  33132  sat1el2xp  33241  untelirr  33549  untsucf  33551  dfon2lem4  33668  dfon2lem6  33670  dfon2lem7  33671  dfon2lem8  33672  dfon2  33674  sltval2  33786  nogt01o  33826  madebdayim  33997  madebdaylemlrcut  34006  fwddifnp1  34394  domalom  35502  pibt2  35515  poimirlem18  35722  poimirlem21  35725  heibor1lem  35894  heiborlem4  35899  heiborlem6  35901  atlex  37257  psubspi  37688  elpcliN  37834  ldilval  38054  trlord  38510  tendotp  38702  hdmapval2  39773  pwelg  41056  gneispace0nelrn2  41640  gneispaceel2  41643  gneispacess2  41645  stoweid  43494  iccpartimp  44757  iccpartltu  44765  iccpartgtl  44766  iccpartleu  44768  iccpartgel  44769  isomushgr  45166  isomuspgrlem1  45167  isomuspgr  45174  isomgrtrlem  45178  1arymaptf1  45876