Theorem rspccv 3619

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062

This theorem is referenced by:  elinti  4955  trss  5270  fvn0ssdmfun  7094  dff3  7120  2fvcoidd  7317  ofrval  7709  limsuc  7870  limuni3  7873  peano5  7915  frxp  8151  wfrdmclOLD  8357  smo11  8404  odi  8617  supub  9499  suplub  9500  elirrv  9636  dfom3  9687  noinfep  9700  tcrank  9924  alephle  10128  dfac5lem5  10167  dfac2b  10171  cofsmo  10309  coftr  10313  infpssrlem4  10346  isf34lem6  10420  axcc2lem  10476  domtriomlem  10482  axdc2lem  10488  axdc3lem2  10491  axdc4lem  10495  ac5b  10518  zorn2lem2  10537  zorn2lem6  10541  pwcfsdom  10623  inar1  10815  grupw  10835  grupr  10837  gruurn  10838  grothpw  10866  grothpwex  10867  axgroth6  10868  grothomex  10869  nqereu  10969  supsrlem  11151  axpre-sup  11209  dedekind  11424  dedekindle  11425  supmullem1  12238  supmul  12240  peano5nni  12269  dfnn2  12279  peano5uzi  12707  zindd  12719  lcmfdvds  16679  lcmfunsn  16681  1arith  16965  ramcl  17067  clatleglb  18563  pslem  18617  cyccom  19221  rngisomring1  20468  psgndiflemA  21619  eqcoe1ply1eq  22303  mvmumamul1  22560  smadiadetlem0  22667  chpscmat  22848  basis2  22958  tg2  22972  clsndisj  23083  cnpimaex  23264  t1sncld  23334  regsep  23342  nrmsep3  23363  cmpsub  23408  2ndc1stc  23459  refssex  23519  ptfinfin  23527  txcnpi  23616  txcmplem1  23649  tx1stc  23658  filss  23861  ufilss  23913  fclsopni  24023  fclsrest  24032  alexsubb  24054  alexsubALTlem2  24056  alexsubALTlem4  24058  ghmcnp  24123  qustgplem  24129  mopni  24505  metrest  24537  metcnpi  24557  metcnpi2  24558  nmolb  24738  nmoleub2lem2  25149  ovoliunlem1  25537  ovolicc2lem3  25554  mblsplit  25567  fta1b  26211  plycj  26317  plycjOLD  26319  lgamgulmlem1  27072  sqfpc  27180  ostth2lem2  27678  ostth3  27682  sltval2  27701  nogt01o  27741  madebdayim  27926  madebdaylemlrcut  27937  precsexlem9  28239  dfn0s2  28336  peano5uzs  28390  vdiscusgr  29549  0vtxrusgr  29595  rusgrnumwrdl2  29604  ewlkinedg  29622  eupthseg  30225  upgreupthseg  30228  numclwwlk1  30380  l2p  30498  lpni  30499  nvz  30688  chcompl  31261  ocin  31315  hmopidmchi  32170  dmdmd  32319  dmdbr5  32327  mdsl1i  32340  sigaclci  34133  bnj23  34732  kur14lem9  35219  sconnpht  35234  cvmsdisj  35275  sat1el2xp  35384  untelirr  35708  untsucf  35710  dfon2lem4  35787  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon2  35793  fwddifnp1  36166  domalom  37405  pibt2  37418  poimirlem18  37645  poimirlem21  37648  heibor1lem  37816  heiborlem4  37821  heiborlem6  37823  atlex  39317  psubspi  39749  elpcliN  39895  ldilval  40115  trlord  40571  tendotp  40763  hdmapval2  41834  cantnfresb  43337  pwelg  43573  gneispace0nelrn2  44154  gneispaceel2  44157  gneispacess2  44159  stoweid  46078  iccpartimp  47404  iccpartltu  47412  iccpartgtl  47413  iccpartleu  47415  iccpartgel  47416  isuspgrim0  47872  gricushgr  47886  1arymaptf1  48563