Theorem rspccv 3279

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175

This theorem is referenced by:  elinti  4420  trss  4689  fvn0ssdmfun  6258  dff3  6280  2fvcoidd  6452  ofrval  6805  limsuc  6941  limuni3  6944  frxp  7174  wfrdmcl  7310  smo11  7348  odi  7546  supub  8248  suplub  8249  elirrv  8387  dfom3  8427  noinfep  8440  oemapvali  8464  tcrank  8630  infxpenlem  8719  alephle  8794  dfac5lem5  8833  dfac2  8836  cofsmo  8974  coftr  8978  infpssrlem4  9011  isf34lem6  9085  axcc2lem  9141  domtriomlem  9147  axdc2lem  9153  axdc3lem2  9156  axdc4lem  9160  ac5b  9183  zorn2lem2  9202  zorn2lem6  9206  pwcfsdom  9284  inar1  9476  grupw  9496  grupr  9498  gruurn  9499  grothpw  9527  grothpwex  9528  axgroth6  9529  grothomex  9530  nqereu  9630  supsrlem  9811  axpre-sup  9869  dedekind  10079  dedekindle  10080  supmullem1  10870  supmul  10872  peano5nni  10900  dfnn2  10910  peano5uzi  11342  zindd  11354  1arith  15469  ramcl  15571  clatleglb  16949  pslem  17029  cygabl  18115  eqcoe1ply1eq  19488  psgndiflemA  19766  mvmumamul1  20179  smadiadetlem0  20286  chpscmat  20466  basis2  20566  tg2  20580  clsndisj  20689  cnpimaex  20870  t1sncld  20940  regsep  20948  nrmsep3  20969  cmpsub  21013  2ndc1stc  21064  refssex  21124  ptfinfin  21132  txcnpi  21221  txcmplem1  21254  tx1stc  21263  filss  21467  ufilss  21519  fclsopni  21629  fclsrest  21638  alexsubb  21660  alexsubALTlem2  21662  alexsubALTlem4  21664  ghmcnp  21728  qustgplem  21734  mopni  22107  metrest  22139  metcnpi  22159  metcnpi2  22160  cfilucfil  22174  nmolb  22331  nmoleub2lem2  22724  ovoliunlem1  23077  ovolicc2lem3  23094  mblsplit  23107  fta1b  23733  plycj  23837  mtest  23962  lgamgulmlem1  24555  sqfpc  24663  ostth2lem2  25123  ostth3  25127  vdiscusgra  26448  rusgranumwwlkl1  26473  usgn0fidegnn0  26556  numclwwlk1  26625  lpni  26722  nvz  26908  ubthlem2  27111  chcompl  27483  ocin  27539  hmopidmchi  28394  dmdmd  28543  dmdbr5  28551  mdsl1i  28564  sigaclci  29522  bnj23  30038  kur14lem9  30450  sconpht  30465  cvmsdisj  30506  untelirr  30839  untsucf  30841  dfon2lem4  30935  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  dfon2  30941  frrlem5e  31032  sltval2  31053  fwddifnp1  31442  poimirlem18  32597  poimirlem21  32600  heibor1lem  32778  heiborlem4  32783  heiborlem6  32785  atlex  33621  psubspi  34051  elpcliN  34197  ldilval  34417  trlord  34875  tendotp  35067  hdmapval2  36142  pwelg  36884  gneispace0nelrn2  37459  gneispaceel2  37462  gneispacess2  37464  stoweid  38956  iccpartltu  39963  iccpartgtl  39964  iccpartleu  39966  iccpartgel  39967  nbgrnself2  40585  vdiscusgr  40747  rusgrnumwrdl2  40786  ewlkinedg  40806  av-numclwwlk1  41528  ssdifsn  42228